remove unused scripts

YaelDillies · Nov 14, 2023 · 1cba5b1 · 1cba5b1
1 parent 44307cc
commit 1cba5b1
Show file tree

Hide file tree

Showing 7 changed files with 2 additions and 183 deletions.
diff --git a/Dockerfile b/Dockerfile
diff --git a/scripts/detect_errors.py b/scripts/detect_errors.py
diff --git a/scripts/fetch_olean_cache.sh b/scripts/fetch_olean_cache.sh
diff --git a/scripts/get_cache.sh b/scripts/get_cache.sh
diff --git a/scripts/mk_all.sh b/scripts/mk_all.sh
@@ -6,8 +6,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 `LeanCamCombi.lean`.
 
 cd "$( dirname "${BASH_SOURCE[0]}" )"/../LeanCamCombi
 if [[ $# = 1 ]]; then

diff --git a/scripts/nolints.txt b/scripts/nolints.txt
diff --git a/scripts/update_nolints.sh b/scripts/update_nolints.sh