diff options
Diffstat (limited to 'doc/manual/example7')
| -rw-r--r-- | doc/manual/example7/gen.sh | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/doc/manual/example7/gen.sh b/doc/manual/example7/gen.sh index 6fb971e..c44676f 100644 --- a/doc/manual/example7/gen.sh +++ b/doc/manual/example7/gen.sh @@ -2,13 +2,13 @@ JAVA=java GLUEGEN_JAR=../../../build/gluegen.jar -ANTLR_JAR=../../../../../ANTLR/antlr-2.7.4/antlr.jar +ANTLR_JAR=../../../../../ANTLR/antlr-2.7.5.jar NAME=`uname` -if [ $NAME="Windows*" ] ; then +if [[ $NAME == "Windows*" ]] ; then SEP=\; -elif [ $NAME="CYGWIN*" ] ; then +elif [[ $NAME == "CYGWIN*" ]] ; then SEP=\; else SEP=: |