diff options
Diffstat (limited to 'debian/patches/manual-build.patch')
| -rw-r--r-- | debian/patches/manual-build.patch | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/debian/patches/manual-build.patch b/debian/patches/manual-build.patch index e6504174..9f1ee9cd 100644 --- a/debian/patches/manual-build.patch +++ b/debian/patches/manual-build.patch @@ -1,6 +1,6 @@ -Description: build the manual using the headers from the source tree, not +Subject: build the manual using the headers from the source tree, not the installed ones. -Author: Sebastian Kuzminsky <seb@highlab.com> +From: Sebastian Kuzminsky <seb@highlab.com> Index: yosys/manual/PRESENTATION_Prog/Makefile =================================================================== --- yosys.orig/manual/PRESENTATION_Prog/Makefile 2016-02-28 22:25:29.557021857 -0700 |