| changeset 42124 | 7519c7c33017 |
| parent 42077 | 96c50a4210a2 |
| child 48858 | 86816c61b5ca |
| 42123:c407078c0d47 | 42124:7519c7c33017 |
|---|---|
53 |
53 |
54 for DIR in "${TOOLS[@]}" |
54 for DIR in "${TOOLS[@]}" |
55 do |
55 do |
56 TOOL="$DIR/$TOOLNAME" |
56 TOOL="$DIR/$TOOLNAME" |
57 case "$TOOL" in |
57 case "$TOOL" in |
58 *~) ;; |
58 *~ | *.orig) ;; |
59 *) [ -f "$TOOL" -a -x "$TOOL" ] && exec "$TOOL" "$@" ;; |
59 *) [ -f "$TOOL" -a -x "$TOOL" ] && exec "$TOOL" "$@" ;; |
60 esac |
60 esac |
61 done |
61 done |
62 |
62 |
63 fail "Unknown Isabelle tool: $TOOLNAME" |
63 fail "Unknown Isabelle tool: $TOOLNAME" |