Skip to content

Commit

Permalink
chore: fix test_mathlib.yml (5) (#964)
Browse files Browse the repository at this point in the history
  • Loading branch information
kim-em authored Sep 27, 2024
1 parent d3d6925 commit e023a81
Showing 1 changed file with 2 additions and 1 deletion.
3 changes: 2 additions & 1 deletion .github/workflows/test_mathlib.yml
Original file line number Diff line number Diff line change
Expand Up @@ -74,7 +74,8 @@ jobs:
echo "Branch does not exist, creating it."
git switch -c batteries-pr-testing-$PR_NUMBER "$BASE"
sed -i 's,require "leanprover-community" / "batteries" @ git ".\+",require "leanprover-community" / "batteries" from git "https://github.com/$HEAD_REPO" @ "$HEAD_BRANCH",' lakefile.lean
# Use the fork and branch name to modify the lakefile.lean
sed -i "s,require \"leanprover-community\" / \"batteries\" @ git \".\+\",require \"leanprover-community\" / \"batteries\" from git \"https://github.com/$HEAD_REPO\" @ \"$HEAD_BRANCH\",g" lakefile.lean
lake update batteries
git add lakefile.lean lake-manifest.json
Expand Down

0 comments on commit e023a81

Please sign in to comment.