author | wenzelm |
Sun, 18 Nov 2012 16:31:41 +0100 | |
changeset 50120 | 245f5947233c |
parent 50119 | 5c370a036de7 |
child 50121 | 97d2b77313a0 |
--- a/src/Tools/jEdit/lib/Tools/jedit Sun Nov 18 16:04:13 2012 +0100 +++ b/src/Tools/jEdit/lib/Tools/jedit Sun Nov 18 16:31:41 2012 +0100 @@ -153,7 +153,7 @@ # args if [ "$#" -eq 0 ]; then - ARGS["${#ARGS[@]}"]="$USER_HOME/Scratch.thy" + ARGS["${#ARGS[@]}"]="$(jvmpath "$USER_HOME/Scratch.thy")" else while [ "$#" -gt 0 ]; do ARGS["${#ARGS[@]}"]="$(jvmpath "$1")"