diff options
| author | P. J. McDermott <pj@pehjota.net> | 2014-05-07 13:17:05 (EDT) |
|---|---|---|
| committer | P. J. McDermott <pj@pehjota.net> | 2014-05-07 13:17:05 (EDT) |
| commit | af5d5b31625974ab0384ab0b3f301ad804240ed7 (patch) | |
| tree | dedd8efe8ee00c0e5367ba2dfb9bb61f80ce63f7 /build | |
| parent | 6b8e4081f0e47ed7926598ce86601e3345041458 (diff) | |
build: Disable makeinfo runs.
Diffstat (limited to 'build')
| -rwxr-xr-x | build | 4 |
1 files changed, 2 insertions, 2 deletions
@@ -10,11 +10,11 @@ configure: touch $@ build: configure - oh-autobuild + oh-autobuild -- MAKEINFO=: touch $@ install: build - oh-autoinstall + oh-autoinstall -- MAKEINFO=: mv dest/usr/bin/dc dest/usr/bin/dc.gnu # Remove GNU Info index. rm -f dest/usr/share/info/dir |