more robust wrt. spaces in directory names;
--- 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 "$@"