Allow build's clean options to be given in any mix of letter-cases

HOL-Theorem-Prover · Jan 4, 2024 · 7818249 · 7818249
1 parent a1eb6e6
commit 7818249
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 3 deletions.
diff --git a/tools/buildhelp.txt b/tools/buildhelp.txt
@@ -21,4 +21,7 @@ OR
   build [--nograph|--graph] help
     builds the help system only
 
+The clean* variations can be given in whatever mix of letter-cases
+desired (i.e., "cleanall" and "Cleanall" work as well as "cleanAll").
+
 Options:
diff --git a/tools/buildutils.sml b/tools/buildutils.sml
@@ -317,10 +317,12 @@ fun get_cline () = let
                               errFn = cline_die } (CommandLine.arguments())
   val option_record = apply_updates opts buildcline.initial
   val _ = if #help option_record then exit_with_help() else ()
+  fun lcnorm_mem s list =
+      List.exists (fn s' => CharVector.map Char.toLower s' = s) list
   val _ =
-      if mem "cleanAll" rest then raise DoClean "cleanAll"
-      else if mem "clean" rest then raise DoClean "clean"
-      else if mem "cleanForReloc" rest then raise DoClean "cleanForReloc"
+      if lcnorm_mem "cleanall" rest then raise DoClean "cleanAll"
+      else if lcnorm_mem "clean" rest then raise DoClean "clean"
+      else if lcnorm_mem "cleanforreloc" rest then raise DoClean "cleanForReloc"
       else ()
   val seqspec =
       case #seqname option_record of