From ae5e7cd4b367be5e80a3d6d8f86f6ecf38f30695 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Sun, 5 Dec 2021 19:54:45 +0000 Subject: [PATCH] chore(scripts/mk_all.sh): allow 'mk_all.sh ../test' (#10628) Helpful for mathport CI, cf https://github.com/leanprover-community/mathport/pull/64 Co-authored-by: Scott Morrison --- scripts/mk_all.sh | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/scripts/mk_all.sh b/scripts/mk_all.sh index 8d4c3cdebf309..b9679e7211308 100755 --- a/scripts/mk_all.sh +++ b/scripts/mk_all.sh @@ -4,17 +4,23 @@ # Examples: # ./scripts/mk_all.sh # ./scripts/mk_all.sh data/real +# ./scripts/mk_all.sh ../archive # # Makes a mathlib/src/$directory/all.lean importing all files inside $directory. # If $directory is omitted, creates `mathlib/src/all.lean`. cd "$( dirname "${BASH_SOURCE[0]}" )"/../src if [[ $# = 1 ]]; then - dir="$1" + dir="${1%/}" # remove trailing slash if present else dir="." fi +# remove an initial `./` +# replace an initial `../test/` with just `.` (similarly for `roadmap`/`archive`/...) +# replace all `/` with `.` +# strip the `.lean` suffix +# prepend `import ` find "$dir" -name \*.lean -not -name all.lean \ - | sed 's,^\./,,;s,\.lean$,,;s,/,.,g;s,^,import ,' \ + | sed 's,^\./,,;s,^\.\./[^/]*,,;s,/,.,g;s,\.lean$,,;s,^,import ,' \ | sort >"$dir"/all.lean