diff --git a/bin/jgf2+ b/bin/jgf2+ deleted file mode 100644 index a452d34cc..000000000 --- a/bin/jgf2+ +++ /dev/null @@ -1,12 +0,0 @@ -#! /bin/sh - -# change the value of GFHOME to the directory where you have the gf binary -GFHOME=/home/aarne/GF2/bin - # /.../chalmers.se/fs/cab/cs/.users/markus/home/GF1 - -JGUILIB=$GFHOME/java/ -GF=$GFHOME/gf2+ -JGUI=GFEditor2 - -java -cp $JGUILIB $JGUI "$GF -java -new $*" -