diff options
author | Stephane Glondu <steph@glondu.net> | 2012-09-22 12:31:59 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2012-09-22 12:51:26 +0200 |
commit | dcdaa8517bfaedcf4ce97380d39011d976fc1b64 (patch) | |
tree | 17e03b2777b9afeb51975b44d7493cccc43ec077 /debian/patches/series | |
parent | e0356f0d6ec9310a3863f1983f7264847be3c274 (diff) |
Upstream bugfix: Fix use of $(HASNATDYNLINK) in coq_makefile output
Diffstat (limited to 'debian/patches/series')
-rw-r--r-- | debian/patches/series | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/debian/patches/series b/debian/patches/series index 53d51a16..f1d97c91 100644 --- a/debian/patches/series +++ b/debian/patches/series @@ -1 +1,2 @@ 0001-test-suite-success-Nsatz.v-comment-out-Ceva.patch +0002-Fix-use-of-HASNATDYNLINK-in-coq_makefile-output.patch |