From af5d5b31625974ab0384ab0b3f301ad804240ed7 Mon Sep 17 00:00:00 2001
From: P. J. McDermott <pj@pehjota.net>
Date: Wed, 07 May 2014 13:17:05 -0400
Subject: build: Disable makeinfo runs.

---
(limited to 'build')

diff --git a/build b/build
index 21410e4..1d44950 100755
--- a/build
+++ b/build
@@ -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
--
cgit v0.9.1