author | wenzelm |
Fri, 26 Jun 2009 21:52:56 +0200 | |
changeset 34631 | 83cf912efd8a |
parent 34630 | 9ba00a967121 |
child 34632 | f044d8446ae9 |
--- a/src/Tools/jEdit/dist-template/interface Fri Jun 26 21:47:22 2009 +0200 +++ b/src/Tools/jEdit/dist-template/interface Fri Jun 26 21:52:56 2009 +0200 @@ -73,7 +73,7 @@ declare -a FILES=() if [ "$#" -eq 0 ]; then - FILES+=($(jvmpath "$HOME/Scratch.thy")) + FILES+=(Scratch.thy) else while [ "$#" -gt 0 ]; do FILES+=($(jvmpath "$1"))