diff options
| author | rsiddharth <rsd@gnu.org> | 2019-05-19 11:11:22 -0400 |
|---|---|---|
| committer | rsiddharth <rsd@gnu.org> | 2019-05-19 11:11:22 -0400 |
| commit | 46b62a446ee138d67293c1b207d76d6b05ba9223 (patch) | |
| tree | 1a3d847aab53b8c6fb7414cf976bef146c58b146 /MANIFEST.in | |
| parent | d47ca2bb6a64d08007e709cc94d1523bb90ee82b (diff) | |
Makefile: Add GNU_MAKE.
* Makefile (GNU_MAKE): New variable.
(docs): Use GNU Make.
(clean-docs): Use GNU Make.
Diffstat (limited to 'MANIFEST.in')
0 files changed, 0 insertions, 0 deletions