diff options
| author | Zbigniew Jędrzejewski-Szmek <zbyszek@in.waw.pl> | 2014-09-25 17:39:56 -0400 |
|---|---|---|
| committer | Zbigniew Jędrzejewski-Szmek <zbyszek@in.waw.pl> | 2014-09-25 18:19:04 -0400 |
| commit | 0b094b10b4268383c836fa4f285e02ba25ed3ad0 (patch) | |
| tree | 5b248510e613c4a1a6ef81a60a6dac26f85a5679 | |
| parent | ef99aec4d25087dec995b3f00b6957dcee6b13e9 (diff) | |
build-sys: do not distribute make-man-rules.py
It was added to EXTRA_DIST in 3c3e5f4276a893791110b03984735654372aa33a,
but this script only makes sense for developers.
| -rw-r--r-- | Makefile.am | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/Makefile.am b/Makefile.am index 065d688ebb..bf860cdc00 100644 --- a/Makefile.am +++ b/Makefile.am @@ -720,7 +720,6 @@ EXTRA_DIST += \ $(man_MANS) \ tools/make-man-index.py \ tools/make-directive-index.py \ - tools/make-man-rules.py \ tools/xml_helper.py # ------------------------------------------------------------------------------ |