Merge branch 'p/fix-changes-html' into p/38229/korean-translations-TEST

kwankyu · Jun 25, 2024 · 8a9575c · 8a9575c
2 parents c1a234c + 3cd72ed
commit 8a9575c
Showing 1 changed file with 8 additions and 6 deletions.
diff --git a/.github/workflows/doc-build.yml b/.github/workflows/doc-build.yml
@@ -150,7 +150,7 @@ jobs:
            git init && \
            (echo "*.svg binary"; echo "*.pdf binary") >> .gitattributes && \
            (echo ".buildinfo"; echo '*.inv'; echo '.git*'; echo '*.svg'; echo '*.pdf'; echo '*.png'; echo 'searchindex.js') > .gitignore; \
-           git add -A && git commit --quiet -m "old")
+           git add -A && git commit --quiet -m 'old')
 
       - name: Build doc
         id: docbuild
@@ -175,13 +175,15 @@ jobs:
           docker cp --follow-link BUILD:/sage/local/share/doc/sage/html doc
           docker cp --follow-link BUILD:/sage/local/share/doc/sage/index.html doc
           (cd doc && git commit -a -m 'new')
-          # Wipe out chronic diffs of new doc against old doc
+          # Wipe out chronic diffs of new doc against old doc before creating changes.html
           (cd doc && \
            find . -name "*.html" | xargs sed -i -e '/This is documentation for/ s/ built with GitHub PR .*. Doc/. Doc/' \
-                                                -e '/<link rel="stylesheet"/ s/?v=[0-9a-f]*"/"/')
-          .ci/create-changes-html.sh $(cd doc && git rev-parse HEAD^) doc
-          # Restore the new doc from changes by "wipe out"
-          (cd doc && git checkout -f)
+                                                -e '/<link rel="stylesheet"/ s/?v=[0-9a-f]*"/"/' \
+           && git commit -a -m 'chronic-diff')
+          # Since HEAD is at commit 'chronic-diff', HEAD~1 is commit 'new' (new doc), HEAD~2 is commit 'old' (old doc)
+          .ci/create-changes-html.sh $(cd doc && git rev-parse HEAD~2) doc
+          # Restore the new doc with changes made in create-changes-html.sh but dropping changes by "wipe out"
+          (cd doc && git stash && git checkout -f HEAD~1 && git stash pop)
           # Sometimes rm -rf .git errors out because of some diehard hidden files
           # So we simply move it out of the doc directory
           (cd doc && mv .git ../git && mv .gitattributes ../gitattributes)