more robust wrt. spaces in directory names;
authorwenzelm
Wed, 02 May 2012 13:09:26 +0200
changeset 47848 030d3c89eacf
parent 47847 7cddb6c8f93c
child 47849 48b52cdc214a
more robust wrt. spaces in directory names;
src/HOL/Mirabelle/lib/Tools/mirabelle
--- a/src/HOL/Mirabelle/lib/Tools/mirabelle	Wed May 02 11:47:45 2012 +0200
+++ b/src/HOL/Mirabelle/lib/Tools/mirabelle	Wed May 02 13:09:26 2012 +0200
@@ -7,17 +7,17 @@
 
 PRG="$(basename "$0")"
 
-function print_action_names() {
-  TOOLS="$MIRABELLE_HOME/Tools/mirabelle_*.ML"
-  for TOOL in $TOOLS
+function print_action_names()
+{
+  for TOOL in "$MIRABELLE_HOME/Tools"/mirabelle_*.ML
   do
-    echo $TOOL | perl -w -p -e 's/.*mirabelle_(.*)\.ML/    $1/'
+    echo "$TOOL" | perl -w -p -e 's/.*mirabelle_(.*)\.ML/    $1/'
   done
 }
 
 function print_sledgehammer_options() {
-  grep -e "^val .*K =" $MIRABELLE_HOME/Tools/mirabelle_sledgehammer.ML \
-  | perl -w -p -e 's/val .*K *= *"(.*)" *\(\*(.*)\*\)/    $1$2/'
+  grep -e "^val .*K =" "$MIRABELLE_HOME/Tools/mirabelle_sledgehammer.ML" | \
+  perl -w -p -e 's/val .*K *= *"(.*)" *\(\*(.*)\*\)/    $1$2/'
 }
 
 function usage() {
@@ -107,6 +107,7 @@
 
 export MIRABELLE_OUTPUT_PATH
 
+
 ## main
 
 for FILE in "$@"