author | wenzelm |
Fri, 26 Jun 2009 18:23:30 +0200 | |
changeset 34622 | b1b88879c515 |
parent 34621 | 6cba4b3723e4 |
child 34623 | a356a8ee6f00 |
--- a/src/Tools/jEdit/dist-template/interface Fri Jun 26 18:22:40 2009 +0200 +++ b/src/Tools/jEdit/dist-template/interface Fri Jun 26 18:23:30 2009 +0200 @@ -73,10 +73,10 @@ declare -a FILES=() if [ "$#" -eq 0 ]; then - FILES+=("isabelle:$HOME/Scratch.thy") + FILES+=($(jvmpath "$HOME/Scratch.thy")) else while [ "$#" -gt 0 ]; do - FILES+=("isabelle:$1") + FILES+=($(jvmpath "$1")) shift done fi