diff options
| -rw-r--r-- | debian/patches/series | 1 | ||||
| -rw-r--r-- | debian/patches/use-debian-paths.diff | 15 |
2 files changed, 16 insertions, 0 deletions
diff --git a/debian/patches/series b/debian/patches/series new file mode 100644 index 0000000..5df8e5d --- /dev/null +++ b/debian/patches/series @@ -0,0 +1 @@ +use-debian-paths.diff diff --git a/debian/patches/use-debian-paths.diff b/debian/patches/use-debian-paths.diff new file mode 100644 index 0000000..7db995e --- /dev/null +++ b/debian/patches/use-debian-paths.diff @@ -0,0 +1,15 @@ +Description: Use Debian's copyright file + Don't reference a nonexistent upstream LICENSE file. +Author: Benjamin Barenblat <bbaren@mit.edu> +Forwarded: not-needed +--- a/README ++++ b/README +@@ -25,7 +25,7 @@ COPYRIGHT: + The CompCert verified compiler is Copyright 2004, 2005, 2006, 2007, + 2008, 2009, 2010, 2011, 2012, 2013, 2014 Institut National de Recherche en + Informatique et en Automatique (INRIA). It is distributed under the +-conditions stated in file LICENSE. ++conditions stated in file /usr/share/doc/compcert/copyright. + + + CONTACT: |