Fix a bug in doc-build workflow

kwankyu · Nov 1, 2024 · 15d2b4f · 15d2b4f
1 parent 5e03142
commit 15d2b4f
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 3 deletions.
diff --git a/.github/workflows/doc-build.yml b/.github/workflows/doc-build.yml
@@ -195,7 +195,7 @@ jobs:
           fi
           # If so, then create CHANGES.html
           if [[ -n "$PR_NUMBER" ]]; then
-            (cd doc && git commit -a -m 'new')
+            (cd doc && git add -A && git commit --quiet -m 'new')
             # 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/ s/ built with GitHub PR .* for development/ for development/' \

diff --git a/src/doc/Makefile b/src/doc/Makefile
@@ -67,9 +67,7 @@ doc-html-other: doc-html-reference
 
 doc-html: doc-html-reference doc-html-other
 	SAGE_DOC=$$(sage --python -c "from sage.env import SAGE_DOC; print(SAGE_DOC)")
-	find $${SAGE_DOC}/html -type d -path "*/jupyter_execute"
 	find $${SAGE_DOC}/html -type d -path "*/jupyter_execute" -exec rm -rf {} +
-	find $${SAGE_DOC}/html -type d -path "*/jupyter_execute"
 
 # Matches doc-pdf--developer, doc-pdf--reference-manifolds etc.
 doc-pdf--%: