|
|
| version 1.18, 2002/04/03 15:08:27 | version 1.19.2.1, 2002/06/10 11:12:01 |
|---|---|
| Line 734 fi | Line 734 fi |
| PACKAGE=parser | PACKAGE=parser |
| VERSION=3.0b | VERSION=3.0.0002 |
| if test "`cd $srcdir && pwd`" != "`pwd`" && test -f $srcdir/config.status; then | if test "`cd $srcdir && pwd`" != "`pwd`" && test -f $srcdir/config.status; then |
| { echo "configure: error: source directory already configured; run "make distclean" there first" 1>&2; exit 1; } | { echo "configure: error: source directory already configured; run "make distclean" there first" 1>&2; exit 1; } |