From 441a6c7fff46bce0e64e6b0fb8293f003841053b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Fri, 14 Jun 2024 18:31:53 +0000
Subject: [PATCH] Restore `mk_all.sh` Seems like `lake exe mk_all` has some
 hiccups.

---
 scripts/mk_all.sh | 26 ++++++++++++++++++++++++++
 1 file changed, 26 insertions(+)
 create mode 100755 scripts/mk_all.sh

diff --git a/scripts/mk_all.sh b/scripts/mk_all.sh
new file mode 100755
index 0000000000..4b6033fb00
--- /dev/null
+++ b/scripts/mk_all.sh
@@ -0,0 +1,26 @@
+#!/usr/bin/env bash
+# Usage: mk_all.sh [subdirectory]
+#
+# Examples:
+#   ./scripts/mk_all.sh
+#   ./scripts/mk_all.sh data/real
+#   ./scripts/mk_all.sh ../archive
+#
+# Makes a $directory/../$directory.lean file importing all files inside $directory.
+# If $directory is omitted, creates `LeanCamCombi.lean`.
+
+cd "$( dirname "${BASH_SOURCE[0]}" )"/../LeanCamCombi
+if [[ $# = 1 ]]; then
+  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 `».«`
+# replace the `.lean` suffix with `»`
+# prepend `import «`
+find "$dir" -name \*.lean -not -name LeanCamCombi.lean \
+  | sed 's,^\./,,;s,^\.\./[^/]*,,;s,/,.,g;s,\.lean$,,;s,^,import LeanCamCombi.,' \
+  | sort >"$dir"/../LeanCamCombi.lean