todo for fixing mk_all.sh

YaelDillies · Nov 14, 2023 · 356b326 · 356b326
1 parent 1219ecf
commit 356b326
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 3 deletions.
diff --git a/LeanAPAP.lean b/LeanAPAP.lean
@@ -11,10 +11,10 @@ import LeanAPAP.Mathlib.Algebra.Group.Basic
 import LeanAPAP.Mathlib.Algebra.Group.Equiv.Basic
 import LeanAPAP.Mathlib.Algebra.Group.Hom.Defs
 import LeanAPAP.Mathlib.Algebra.Group.Hom.Instances
+import LeanAPAP.Mathlib.Algebra.Group.TypeTags
 import LeanAPAP.Mathlib.Algebra.GroupPower.Basic
 import LeanAPAP.Mathlib.Algebra.GroupPower.Hom
 import LeanAPAP.Mathlib.Algebra.GroupPower.Order
-import LeanAPAP.Mathlib.Algebra.Group.TypeTags
 import LeanAPAP.Mathlib.Algebra.Module.Basic
 import LeanAPAP.Mathlib.Algebra.Order.LatticeGroup
 import LeanAPAP.Mathlib.Algebra.Order.Ring.Canonical

diff --git a/scripts/mk_all.sh b/scripts/mk_all.sh
@@ -1,3 +1,5 @@
+# TODO: This script currently mishandles the $directory argument
+
 #!/usr/bin/env bash
 # Usage: mk_all.sh [subdirectory]
 #
@@ -6,8 +8,8 @@
 #   ./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`.
+# Makes a $directory/../$directory.lean file importing all files inside $directory.
+# If $directory is omitted, creates `LeanAPAP.lean`.
 
 cd "$( dirname "${BASH_SOURCE[0]}" )"/../LeanAPAP
 if [[ $# = 1 ]]; then