changeset 47730 | 15f4309bb9eb |
parent 47480 | 24d8c9e9dae4 |
child 47846 | bbc3e7bccc61 |
--- a/src/HOL/Mirabelle/lib/Tools/mirabelle Tue Apr 24 13:55:02 2012 +0100 +++ b/src/HOL/Mirabelle/lib/Tools/mirabelle Tue Apr 24 13:59:29 2012 +0100 @@ -8,10 +8,10 @@ PRG="$(basename "$0")" function print_action_names() { - ACTIONS="$MIRABELLE_HOME/Actions/mirabelle_*.ML" - for ACTION in $ACTIONS + TOOLS="$MIRABELLE_HOME/Actions/mirabelle_*.ML" + for TOOL in $TOOLS do - echo $ACTION | perl -w -p -e 's/.*mirabelle_(.*)\.ML/ $1/' + echo $TOOL | perl -w -p -e 's/.*mirabelle_(.*)\.ML/ $1/' done }