changeset 7971 | 023778c8a029 |
parent 3276 | f8bf5e5c1641 |
child 9786 | 270ca580b880 |
7970:a15748c3b7e4 | 7971:023778c8a029 |
---|---|
67 do |
67 do |
68 TOOL=$DIR/$TOOLNAME |
68 TOOL=$DIR/$TOOLNAME |
69 [ -f "$TOOL" -a -x "$TOOL" ] && exec "$TOOL" "$@" |
69 [ -f "$TOOL" -a -x "$TOOL" ] && exec "$TOOL" "$@" |
70 done |
70 done |
71 |
71 |
72 fail "Unknown isabelle tool: $TOOLNAME" |
72 fail "Unknown Isabelle tool: $TOOLNAME" |