equal
deleted
inserted
replaced
2 # |
2 # |
3 # Author: Makarius |
3 # Author: Makarius |
4 # |
4 # |
5 # Default Isabelle application wrapper. |
5 # Default Isabelle application wrapper. |
6 |
6 |
7 exec "$(dirname "$0")"/bin/isabelle jedit -s "$@" |
7 exec "$(dirname "$0")"/bin/isabelle jedit -s -- "$@" |
8 |
8 |