# HG changeset patch
# User wenzelm
# Date 1335956966 -7200
# Node ID 030d3c89eacf9f8017c98d0a846002796c7f26f6
# Parent  7cddb6c8f93c57501e06669b88073c56b0596b78
more robust wrt. spaces in directory names;

diff -r 7cddb6c8f93c -r 030d3c89eacf 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 "$@"