diff options
Diffstat (limited to 'config/Makefile.template')
| -rw-r--r-- | config/Makefile.template | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/config/Makefile.template b/config/Makefile.template index 6161089ae..651985488 100644 --- a/config/Makefile.template +++ b/config/Makefile.template @@ -79,10 +79,6 @@ CAMLTIMEPROF=COQPROFILEFLAG # The best compiler: native (=opt) or bytecode (=byte) if no native compiler BEST=BESTCOMPILER -# For Camlp4 use -P4=$(COQTOP)/bin/$(ARCH)/call_camlp4 -I $(COQTOP)/src/parsing -P4DEP=$(COQTOP)/bin/$(ARCH)/camlp4dep - # Your architecture # Can be obtain by UNIX command arch ARCH=ARCHITECTURE |