Closed mkoeppe closed 1 week ago
@mkoeppe I would like to work on this issue.
@Demon-Sheriff Do you understand why it happens? I have no idea.
The relevant part of the script:
(A) (cd doc && git commit -a -m 'new')
# Wipe out chronic diffs of new doc against old doc before creating CHANGES.html
(B) (cd doc && \
find . -name "*.html" | xargs sed -i -e '/This is documentation/ s/ built with GitHub PR .* for development/ for development/' \
-e '/<link rel="stylesheet"/ s/?v=[0-9a-f]*"/"/' \
-e '\;<script type="application/vnd\.jupyter\.widget-state+json">;,\;</script>; d' \
-e 's;#L[0-9]*";";' \
&& git commit -a -m 'wipe-out')
# Since HEAD is at commit 'wipe-out', HEAD~1 is commit 'new' (new doc), HEAD~2 is commit 'old' (old doc)
(C) .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"
(D) (cd doc && git stash -q && git checkout -q -f HEAD~1 && git stash pop -q)
After (A), we have commits "old" < "new"
After (B), we have commits "old" < "new" < "wipe-out"
After (C), we have some changes on "wipe-out". I want to keep these changes but on "new".
So in (D), git stash -q
stashes the changes, and git checkout -q -f HEAD~1
force-checks out "new" branch, effectively removing changes in "wipe-out", and git stash pop -q
is supposed to recover the stashed changes.
I think I can fix it now. Some radical change is necessary.
Testing the fix with #38468.
The use of
git stash pop
can fail with a merge conflict as seen in https://github.com/sagemath/sage/actions/runs/10232970523/job/28310739740?pr=38224#step:13:74