diff options
Diffstat (limited to 'gnu/packages/patches/metamath-remove-missing-file-refs.patch')
| -rw-r--r-- | gnu/packages/patches/metamath-remove-missing-file-refs.patch | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/gnu/packages/patches/metamath-remove-missing-file-refs.patch b/gnu/packages/patches/metamath-remove-missing-file-refs.patch new file mode 100644 index 0000000000..bc4748de98 --- /dev/null +++ b/gnu/packages/patches/metamath-remove-missing-file-refs.patch @@ -0,0 +1,17 @@ +--- metamath.orig/Makefile.am 2020-01-27 20:43:55.650195602 +0900 ++++ metamath/Makefile.am 2020-01-27 20:44:18.876578014 +0900 +@@ -36,14 +36,6 @@ + mmwtex.c \ + $(noinst_HEADERS) + +-dist_pkgdata_DATA = \ +- big-unifier.mm \ +- demo0.mm \ +- miu.mm \ +- peano.mm \ +- ql.mm \ +- set.mm +- + + EXTRA_DIST = \ + LICENSE.TXT \ |