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 /man/.gitignore | |
| 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.
Diffstat (limited to 'man/.gitignore')
0 files changed, 0 insertions, 0 deletions