diff options
| author | Ludovic Courtès <ludo@gnu.org> | 2020-10-16 22:04:33 +0200 |
|---|---|---|
| committer | Ludovic Courtès <ludo@gnu.org> | 2020-10-17 22:40:17 +0200 |
| commit | 3cd1a7ac51c73ce636c3c36b3f790829c8374e04 (patch) | |
| tree | 811b9f7dd38557217259fad5626e6bb73d706669 /gnu/local.mk | |
| parent | a1b88219e8c18297cf27373a186d7adb9886f165 (diff) | |
doc: Remove 'build.scm' from the source of the manual.
That way we no longer have to rebuild the whole manual when fiddling
with 'build.scm'.
* doc/build.scm <top level>: Define 'select?' and pass it to
'pdf+html-manual'.
Diffstat (limited to 'gnu/local.mk')
0 files changed, 0 insertions, 0 deletions