Skip to content

Commit

Permalink
Merge branch 'ci_fix_incremental_build' into flint3
Browse files Browse the repository at this point in the history
  • Loading branch information
mezzarobba committed Jul 7, 2023
2 parents f69299e + 4f0ebac commit fee7d19
Show file tree
Hide file tree
Showing 2 changed files with 6 additions and 2 deletions.
4 changes: 3 additions & 1 deletion .github/workflows/build.yml
Original file line number Diff line number Diff line change
Expand Up @@ -60,11 +60,13 @@ jobs:
# (This keeps mtimes of unchanged files unchanged and mtimes of changed files newer than unchanged files.)
# Finally we reset the index to "old". (This keeps all mtimes unchanged.)
# The changed files now show up as uncommitted changes.
# The final "git add -N" makes sure that files that were added in "new" do not show
# as untracked files, which would be removed by "git clean -fx".
git worktree add --detach worktree-image
rm -rf /sage/.git && mv worktree-image/.git /sage/
rm -rf worktree-image && ln -s /sage worktree-image
if [ ! -f worktree-image/.gitignore ]; then cp .gitignore worktree-image/; fi
(cd worktree-image && git add -A && git commit --allow-empty -m "old" -a && git tag -f old && git reset --hard new && git reset old)
(cd worktree-image && git add -A && git commit --quiet --allow-empty -m "old" -a && git tag -f old && git reset --hard new && git reset --quiet old && git add -N . && git status)
- name: Incremental build, test changed files (sage -t --new)
id: incremental
Expand Down
4 changes: 3 additions & 1 deletion .github/workflows/doc-build.yml
Original file line number Diff line number Diff line change
Expand Up @@ -44,11 +44,13 @@ jobs:
# (This keeps mtimes of unchanged files unchanged and mtimes of changed files newer than unchanged files.)
# Finally we reset the index to "old". (This keeps all mtimes unchanged.)
# The changed files now show up as uncommitted changes.
# The final "git add -N" makes sure that files that were added in "new" do not show
# as untracked files, which would be removed by "git clean -fx".
git worktree add --detach worktree-image
rm -rf /sage/.git && mv worktree-image/.git /sage/
rm -rf worktree-image && ln -s /sage worktree-image
if [ ! -f worktree-image/.gitignore ]; then cp .gitignore worktree-image/; fi
(cd worktree-image && git add -A && git commit --allow-empty -m "old" -a && git tag -f old && git reset --hard new && git reset old)
(cd worktree-image && git add -A && git commit --quiet --allow-empty -m "old" -a && git tag -f old && git reset --hard new && git reset --quiet old && git add -N . && git status)
# Keep track of changes to built HTML
new_version=$(cat src/VERSION.txt); (cd /sage/local/share/doc/sage/html/en && find . -name "*.html" | xargs sed -i '/class="sidebar-brand-text"/s/Sage [0-9a-z.]* /Sage '$new_version' /'; 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")
Expand Down

0 comments on commit fee7d19

Please sign in to comment.