diff --git a/.github/workflows/doc-build.yml b/.github/workflows/doc-build.yml index b6bd0b1c6e3..01d05b25b5d 100644 --- a/.github/workflows/doc-build.yml +++ b/.github/workflows/doc-build.yml @@ -130,10 +130,10 @@ jobs: new_version=$(docker exec BUILD cat src/VERSION.txt) mkdir -p docs/ docker cp BUILD:/sage/local/share/doc/sage/html docs/ - # Wipe out chronic diffs between old doc and new doc + # Wipe out chronic diffs of old doc against new doc (cd docs && \ find . -name "*.html" | xargs sed -i -e '/class="sidebar-brand-text"/ s/Sage [0-9a-z.]* /Sage '"$new_version"' /' \ - -e '/This is documentation for/ s/ built with GitHub PR [^.]*././' \ + -e '/;,\;; d') # Create git repo from old doc @@ -166,7 +166,13 @@ jobs: docker cp BUILD:/sage/local/share/doc/sage/html docs docker cp BUILD:/sage/local/share/doc/sage/index.html docs (cd docs && git commit -a -m 'new') + # Wipe out chronic diffs of new doc against old doc + (cd docs && \ + find . -name "*.html" | xargs sed -i -e '/This is documentation for/ s/ built with GitHub PR .*. Doc/. Doc/' \ + -e '/