diff options
author | Stephane Glondu <steph@glondu.net> | 2008-09-07 18:58:27 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2008-09-08 00:16:26 +0200 |
commit | b6db9f4f71b806d89cd24db386a6bcdd3b469d31 (patch) | |
tree | 98434e63efec4e958e54e22a63130b391f497033 | |
parent | cdce320e124a3fcba458fad3c638940ce8f993ce (diff) |
Remove obsolete patches
-rw-r--r-- | debian/patches/00list | 4 | ||||
-rwxr-xr-x | debian/patches/check.dpatch | 19 | ||||
-rwxr-xr-x | debian/patches/no-complexity-test.dpatch | 21 | ||||
-rwxr-xr-x | debian/patches/non-native-archs.dpatch | 32 | ||||
-rwxr-xr-x | debian/patches/use-env-in-coq-config.dpatch | 24 |
5 files changed, 0 insertions, 100 deletions
diff --git a/debian/patches/00list b/debian/patches/00list index fb3801fa..e69de29b 100644 --- a/debian/patches/00list +++ b/debian/patches/00list @@ -1,4 +0,0 @@ -no-complexity-test -check -use-env-in-coq-config -non-native-archs diff --git a/debian/patches/check.dpatch b/debian/patches/check.dpatch deleted file mode 100755 index d0cb3907..00000000 --- a/debian/patches/check.dpatch +++ /dev/null @@ -1,19 +0,0 @@ -#! /bin/sh /usr/share/dpatch/dpatch-run -## check.dpatch by Samuel Mimram <smimram@debian.org> -## -## All lines beginning with `## DP:' are a description of the patch. -## DP: Suppress warnings from tests outputs. - -@DPATCH@ -diff -urNad coq~/test-suite/check coq/test-suite/check ---- coq~/test-suite/check 2008-07-25 15:36:31.000000000 +0200 -+++ coq/test-suite/check 2008-07-25 15:36:31.000000000 +0200 -@@ -52,7 +52,7 @@ - nbtests=`expr $nbtests + 1` - printf " "$f"..." - tmpoutput=`mktemp /tmp/coqcheck.XXXXXX` -- $command $f 2>&1 | grep -v "Welcome to Coq" | grep -v "Skipping rcfile loading" > $tmpoutput -+ $command $f 2>&1 | grep -v "Welcome to Coq" | grep -v "Skipping rcfile loading" | grep -v "some rule has been masked" > $tmpoutput - foutput=`dirname $f`/`basename $f .v`.out - diff $tmpoutput $foutput >& /dev/null - if [ $? = 0 ]; then diff --git a/debian/patches/no-complexity-test.dpatch b/debian/patches/no-complexity-test.dpatch deleted file mode 100755 index 5f9bff67..00000000 --- a/debian/patches/no-complexity-test.dpatch +++ /dev/null @@ -1,21 +0,0 @@ -#! /bin/sh /usr/share/dpatch/dpatch-run -## no-complexity-test.dpatch by Julien Cristau <julien.cristau@ens-lyon.org> -## -## All lines beginning with `## DP:' are a description of the patch. -## DP: Don't run complexity tests, they are far too fragile. - -@DPATCH@ -diff -urNad coq~/test-suite/check coq/test-suite/check ---- coq~/test-suite/check 2008-07-25 15:13:00.000000000 +0200 -+++ coq/test-suite/check 2008-07-25 15:33:55.000000000 +0200 -@@ -250,8 +250,8 @@ - test_interactive interactive - echo "Micromega tests" - test_success micromega --echo "Complexity tests" --test_complexity complexity -+echo "Skipping complexity tests" -+#test_complexity complexity - echo "Module tests" - $coqtop -compile modules/Nat - $coqtop -compile modules/plik diff --git a/debian/patches/non-native-archs.dpatch b/debian/patches/non-native-archs.dpatch deleted file mode 100755 index cbb9f832..00000000 --- a/debian/patches/non-native-archs.dpatch +++ /dev/null @@ -1,32 +0,0 @@ -#! /bin/sh /usr/share/dpatch/dpatch-run -## non-native-archs.dpatch by Stephane Glondu <steph@glondu.net> -## -## All lines beginning with `## DP:' are a description of the patch. -## DP: Fix FTBFS on non-native architectures - -@DPATCH@ -diff --git a/Makefile.build b/Makefile.build -index a5bae4e..c47b688 100644 ---- a/Makefile.build -+++ b/Makefile.build -@@ -655,7 +655,10 @@ install-library: - $(MKDIR) $(FULLCOQLIB)/states - $(INSTALLLIB) states/*.coq $(FULLCOQLIB)/states - $(MKDIR) $(FULLCOQLIB)/user-contrib -- $(INSTALLLIB) $(LINKCMO) $(LINKCMX) $(GRAMMARCMA) $(FULLCOQLIB) -+ $(INSTALLLIB) $(LINKCMO) $(GRAMMARCMA) $(FULLCOQLIB) -+ifeq ($(BEST),opt) -+ $(INSTALLLIB) $(LINKCMX) $(FULLCOQLIB) -+endif - find . -name \*.cmi -exec $(INSTALLLIB) {} $(FULLCOQLIB) \; - - install-library-light: -@@ -716,7 +719,7 @@ dev/printers.cma: $(PRINTERSCMO) - parsing/grammar.cma: $(GRAMMARCMO) - $(SHOW)'Testing $@' - @touch test.ml4 -- $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) $(GRAMMARCMO) -impl" -impl test.ml4 -o test-grammar -+ $(HIDE)$(OCAMLC) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) $(GRAMMARCMO) -impl" -impl test.ml4 -o test-grammar - @rm -f test-grammar test.* - $(SHOW)'OCAMLC -a $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) $(GRAMMARCMO) -linkall -a -o $@ diff --git a/debian/patches/use-env-in-coq-config.dpatch b/debian/patches/use-env-in-coq-config.dpatch deleted file mode 100755 index 1f01315f..00000000 --- a/debian/patches/use-env-in-coq-config.dpatch +++ /dev/null @@ -1,24 +0,0 @@ -#! /bin/sh /usr/share/dpatch/dpatch-run -## use-env-in-coq-config.dpatch by Stephane Glondu <steph@glondu.net> -## -## All lines beginning with `## DP:' are a description of the patch. -## DP: Use environment variables by default in coq_config.ml - -@DPATCH@ -diff --git a/configure b/configure -index 2747ee2..a57b996 100755 ---- a/configure -+++ b/configure -@@ -862,9 +862,9 @@ cat << END_OF_COQ_CONFIG > $mlconfig_file - (* DO NOT EDIT THIS FILE: automatically generated by ../configure *) - - let local = $local --let bindir = "$ESCBINDIR" --let coqlib = "$ESCLIBDIR" --let coqtop = "$ESCCOQTOP" -+let bindir = try Sys.getenv "COQBIN" with Not_found -> "$ESCBINDIR" -+let coqlib = try Sys.getenv "COQLIB" with Not_found -> "$ESCLIBDIR" -+let coqtop = try Sys.getenv "COQTOP" with Not_found -> "$ESCCOQTOP" - let camldir = "$ESCCAMLDIR" - let camllib = "$ESCCAMLLIB" - let camlp4 = "$CAMLP4" |