Skip to content

Commit

Permalink
chore: cp -l doesn't work on mac
Browse files Browse the repository at this point in the history
  • Loading branch information
dselsam committed Feb 1, 2022
1 parent 18731e4 commit 4e5c582
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -73,7 +73,7 @@ lean3-predata: lean3-source
find sources/lean/library -name "*.olean" -delete # ast only exported when oleans not present
cd sources/lean && elan override set `cat ../mathlib/leanpkg.toml | grep lean_version | cut -d '"' -f2`
cd sources/lean && lean --make --recursive --ast --tlean library
cp -rl sources/lean/library PreData/Leanbin
cp -r sources/lean/library PreData/Leanbin
find PreData/ -name "*.lean" -delete
find PreData/ -name "*.olean" -delete

Expand All @@ -83,7 +83,7 @@ mathbin-predata: mathbin-source
find sources/mathlib -name "*.olean" -delete # ast only exported when oleans not present
# By changing into the directory, `elan` automatically dispatches to the correct binary.
cd sources/mathlib && lean --make --recursive --ast --tlean src
cp -rl sources/mathlib PreData/Mathbin
cp -r sources/mathlib PreData/Mathbin
find PreData/ -name "*.lean" -delete
find PreData/ -name "*.olean" -delete

Expand Down

2 comments on commit 4e5c582

@gebner
Copy link
Member

@gebner gebner commented on 4e5c582 Feb 2, 2022

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is there a replacement for the -l flag on mac? This flag saves several gigabytes.

@gebner
Copy link
Member

@gebner gebner commented on 4e5c582 Feb 2, 2022

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

       -l, --link
              hard link files instead of copying

Please sign in to comment.