summaryrefslogtreecommitdiff
path: root/debian
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-10-15 17:25:39 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2010-10-15 17:25:39 +0200
commit088c96d71b9151ed6a84ff6dc6087c4d24b12aa0 (patch)
tree710e1d103fbd8a4dcffa4f71b82eda3941de5e9c /debian
parent3fc476cad53735d8fad41a007ae7bee70db16905 (diff)
Add patch to fix test-suite
Diffstat (limited to 'debian')
-rw-r--r--debian/patches/0001-Fix-missing-coqlib-argument-to-coqdep-in-test-suite.patch23
-rw-r--r--debian/patches/series1
2 files changed, 24 insertions, 0 deletions
diff --git a/debian/patches/0001-Fix-missing-coqlib-argument-to-coqdep-in-test-suite.patch b/debian/patches/0001-Fix-missing-coqlib-argument-to-coqdep-in-test-suite.patch
new file mode 100644
index 00000000..c3092bac
--- /dev/null
+++ b/debian/patches/0001-Fix-missing-coqlib-argument-to-coqdep-in-test-suite.patch
@@ -0,0 +1,23 @@
+From: Stephane Glondu <steph@glondu.net>
+Date: Fri, 15 Oct 2010 17:24:18 +0200
+Subject: [PATCH] Fix missing -coqlib argument to coqdep in test-suite
+
+Signed-off-by: Stephane Glondu <steph@glondu.net>
+---
+ test-suite/Makefile | 2 +-
+ 1 files changed, 1 insertions(+), 1 deletions(-)
+
+diff --git a/test-suite/Makefile b/test-suite/Makefile
+index 62d443d..98bab43 100644
+--- a/test-suite/Makefile
++++ b/test-suite/Makefile
+@@ -40,7 +40,7 @@ endif
+
+ command := $(coqtop) -top Top -load-vernac-source
+ coqc := $(coqtop) -compile
+-coqdep := $(BIN)coqdep
++coqdep := $(BIN)coqdep -coqlib $(LIB)
+
+ SHOW := $(if $(VERBOSE),@true,@echo)
+ HIDE := $(if $(VERBOSE),,@)
+--
diff --git a/debian/patches/series b/debian/patches/series
new file mode 100644
index 00000000..c65680e0
--- /dev/null
+++ b/debian/patches/series
@@ -0,0 +1 @@
+0001-Fix-missing-coqlib-argument-to-coqdep-in-test-suite.patch