X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;f=doc%2FMakefile;h=177760e9c6044448d55c05e1527488f1e472b9c6;hb=4f1d12a5e3cef3d0da80e63320fcbc4d46a39c14;hp=c40359bb07e8e34b95cc2e4790800b4bb866d898;hpb=05efa9eaa5690bb85220bcc6af38eb18714c90a9;p=pspp

diff --git a/doc/Makefile b/doc/Makefile
index c40359bb07..177760e9c6 100644
--- a/doc/Makefile
+++ b/doc/Makefile
@@ -7,11 +7,15 @@
 
 doc = gnulib
 
-MAKEINFO = env LANG= LC_MESSAGES= LC_ALL= LANGUAGE= makeinfo
-TEXI2HTML = $(MAKEINFO) --no-split --reference-limit=2000 --html
+lang_env = env LANG= LC_MESSAGES= LC_ALL= LANGUAGE=
+makeinfo_prog = makeinfo
+MAKEINFO = $(lang_env) $(makeinfo_prog)
+
+manual_opts = --no-split --reference-limit=2000
+TEXI2HTML = $(MAKEINFO) $(manual_opts) --html
 
 %.info: %.texi
-	LANG= LC_MESSAGES= LC_ALL= LANGUAGE= makeinfo --no-split --reference-limit=2000 $<
+	$(MAKEINFO) $(manual_opts) $<
 
 %.html: %.texi
 	$(TEXI2HTML) -o $@ $<