From 3cd72edc886b7d855eb20e3090e65737fa77cafa Mon Sep 17 00:00:00 2001 From: Kwankyu Lee Date: Tue, 25 Jun 2024 16:28:20 +0900 Subject: [PATCH] Fix broken changes.html --- .github/workflows/doc-build.yml | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/.github/workflows/doc-build.yml b/.github/workflows/doc-build.yml index 2b75d84c97c..2ea953f70fe 100644 --- 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 '/