diff options
Diffstat (limited to 'camlp4/config/configure_batch')
| -rwxr-xr-x | camlp4/config/configure_batch | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/camlp4/config/configure_batch b/camlp4/config/configure_batch index 36d39c3b40..c5a8ec4407 100755 --- a/camlp4/config/configure_batch +++ b/camlp4/config/configure_batch @@ -70,8 +70,8 @@ echo "O=o" >> Makefile.cnf echo "A=a" >> Makefile.cnf echo "OPT=" >> Makefile.cnf echo "OTOP=$ocaml_top" >> Makefile.cnf -if test -r ../../config/auto_aux/Makefile; then - grep '^RANLIB' ../../config/auto_aux/Makefile >> Makefile.cnf +if test -r ../../config/auto-aux/Makefile; then + grep '^RANLIB' ../../config/auto-aux/Makefile >> Makefile.cnf elif test -r ../../config/Makefile; then grep '^RANLIB' ../../config/Makefile >> Makefile.cnf else |