diff options
| author | aarne <unknown> | 2004-08-10 11:52:42 +0000 |
|---|---|---|
| committer | aarne <unknown> | 2004-08-10 11:52:42 +0000 |
| commit | 470197d442c7a83c2c81c3334485b72ea5921d7f (patch) | |
| tree | f0e6eadb7e641e2ab42a88ab5dab6fd38d6d4ed9 /bin | |
| parent | 310e3e100182d04938d637fbc35fc60679069c84 (diff) | |
clean up
Diffstat (limited to 'bin')
| -rw-r--r-- | bin/jgf2+ | 12 |
1 files changed, 0 insertions, 12 deletions
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 $*" - |