diff options
Diffstat (limited to 'debian/patches/makefile.dpatch')
| -rwxr-xr-x | debian/patches/makefile.dpatch | 20 |
1 files changed, 0 insertions, 20 deletions
diff --git a/debian/patches/makefile.dpatch b/debian/patches/makefile.dpatch deleted file mode 100755 index d16030ca..00000000 --- a/debian/patches/makefile.dpatch +++ /dev/null @@ -1,20 +0,0 @@ -#! /bin/sh /usr/share/dpatch/dpatch-run -## makefile.dpatch by Samuel Mimram <smimram@debian.org> -## -## All lines beginning with `## DP:' are a description of the patch. -## DP: Do not use ocamlopt to test grammar.cma, we don't want to use ocamlopt -## DP: when compiling on non-native archs. - -@DPATCH@ -diff -urNad coq-8.1.pl2+dfsg~/Makefile coq-8.1.pl2+dfsg/Makefile ---- coq-8.1.pl2+dfsg~/Makefile 2007-10-15 11:02:54.000000000 +0000 -+++ coq-8.1.pl2+dfsg/Makefile 2007-10-15 11:03:55.000000000 +0000 -@@ -1479,7 +1479,7 @@ - parsing/grammar.cma: $(GRAMMARCMO) - $(SHOW)'Testing $@' - @touch test.ml4 -- $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENSIONS) $(GRAMMARCMO) -impl" -impl test.ml4 -o test-grammar -+ $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENSIONS) $(GRAMMARCMO) -impl" -impl test.ml4 -o test-grammar - @rm -f test-grammar test.* - $(SHOW)'OCAMLC -a $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) $(GRAMMARCMO) -linkall -a -o $@ |