Skip to content

Commit

Permalink
Fix missing build/make/Makefile error
Browse files Browse the repository at this point in the history
  • Loading branch information
kwankyu committed Feb 18, 2025
1 parent 6578eb6 commit 35f10f9
Showing 1 changed file with 15 additions and 9 deletions.
24 changes: 15 additions & 9 deletions .ci/retrofit-worktree.sh
Original file line number Diff line number Diff line change
Expand Up @@ -20,27 +20,33 @@ git config --global user.email "$GIT_AUTHOR_EMAIL"

set -x

# If actions/checkout downloaded our source tree using the GitHub REST API
# instead of with git, we first make the source tree a repo.
# If actions/checkout downloaded our source tree (in current directory) using the
# GitHub REST API instead of with git, we first make the source tree a repo.
if [ ! -d .git ]; then git init; fi

# Commit and tag this state of the source tree "new". This is what we want to build and test.
# Commit and tag this state of the source tree "new". The current directory
# contains "new" source files with which we want to build and test.
git add -A && git commit --quiet --allow-empty -m "new"
git tag -f new

# Our container image contains a source tree in $WORKTREE_DIRECTORY with a full build of Sage.
# But $WORKTREE_DIRECTORY is not a git repository.
# We make $WORKTREE_DIRECTORY a worktree whose index is at tag "new".
# We then commit the current sources and set the tag "old". (This keeps all mtimes unchanged.)
# Then we update worktree and index with "git checkout new".
# (This keeps mtimes of unchanged files unchanged and mtimes of changed files newer than unchanged files.)
if [ -L $WORKTREE_NAME ]; then
rm -f $WORKTREE_NAME
fi
git worktree prune --verbose
git worktree add --detach $WORKTREE_NAME
rm -rf $WORKTREE_DIRECTORY/.git && mv $WORKTREE_NAME/.git $WORKTREE_DIRECTORY/
rm -rf $WORKTREE_NAME && ln -s $WORKTREE_DIRECTORY $WORKTREE_NAME
if [ ! -f $WORKTREE_NAME/.gitignore ]; then cp .gitignore $WORKTREE_NAME/; cat $WORKTREE_NAME/.gitignore; fi
(cd $WORKTREE_NAME && git status && git add -A && git commit --quiet --allow-empty -m "old" -a && git tag -f old && git checkout -f new && git clean -fd && git status)
(echo "CIDEBUG6:"; ls -l /sage/build/make/Makefile || cat $WORKTREE_NAME/.gitignore)

# Copy "new" .gitignore (in current directory) to the worktree if there is not one already.
if [ ! -f $WORKTREE_NAME/.gitignore ]; then cp .gitignore $WORKTREE_NAME/; fi
# We then commit the worktree and set the tag "old". (This keeps all modification times unchanged.)
(cd $WORKTREE_NAME && git add -A && git commit --quiet --allow-empty -m "old" && git tag -f old)
# Then we update the worktree and index with "git checkout new". (This keeps modification times of "old" files
# and makes modification times of "new" files newer, which triggers incremental build.)
(cd $WORKTREE_NAME && git checkout -f new && \
# For unknown reason, "build/" directory is untracked by git. Hence we force
# it tracked, to avoid removal of "build/make/Makefile" by "git clean -fd"
git add build/ && git clean -fd)

0 comments on commit 35f10f9

Please sign in to comment.