Skip to content

Commit

Permalink
fix(scripts/mk_all): macOS compatibility fix (#4148)
Browse files Browse the repository at this point in the history
`readlink -f` doesn't work macOS unfortunately - there are alternatives but I think it's probably safe to remove it altogether? This assumes `mk_all.sh` isn't a symlink but I can't think of a reason why it should be - and `rm_all.sh` uses `dirname "${BASH_SOURCE[0]}"` directly 🙂
  • Loading branch information
alexpeattie committed Sep 21, 2020
1 parent e483298 commit cd4a91f
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion scripts/mk_all.sh
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@
# Makes a mathlib/src/$directory/all.lean importing all files inside $directory.
# If $directory is omitted, creates `mathlib/src/all.lean`.

cd "$(dirname "$(readlink -f "${BASH_SOURCE[0]}")")"/../src
cd "$( dirname "${BASH_SOURCE[0]}" )"/../src
if [[ $# = 1 ]]; then
dir="$1"
else
Expand Down

0 comments on commit cd4a91f

Please sign in to comment.