equal
deleted
inserted
replaced
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" |