src/HOL/Mirabelle/lib/Tools/mirabelle
changeset 47478 d2392e6cba7f
parent 47477 3fabf352243e
child 47479 e6add51fd7ba
equal deleted inserted replaced
47477:3fabf352243e 47478:d2392e6cba7f
     9 
     9 
    10 function print_action_names() {
    10 function print_action_names() {
    11   ACTIONS="$MIRABELLE_HOME/Actions/mirabelle_*.ML"
    11   ACTIONS="$MIRABELLE_HOME/Actions/mirabelle_*.ML"
    12   for ACTION in $ACTIONS
    12   for ACTION in $ACTIONS
    13   do
    13   do
    14     echo $ACTION | sed 's/.*mirabelle_\(.*\)\.ML/    \1/'
    14     echo $ACTION | perl -w -p -e 's/.*mirabelle_(.*)\.ML/    $1/'
    15   done
    15   done
    16 }
    16 }
    17 
    17 
    18 function usage() {
    18 function usage() {
    19   [ -n "$MIRABELLE_OUTPUT_PATH" ] && out="$MIRABELLE_OUTPUT_PATH" || out="None"
    19   [ -n "$MIRABELLE_OUTPUT_PATH" ] && out="$MIRABELLE_OUTPUT_PATH" || out="None"