diff --git a/Make.mk b/Make.mk index 87968b6b..3cfad4df 100644 --- a/Make.mk +++ b/Make.mk @@ -293,7 +293,7 @@ info.nr/%: info/%.t # Pipes in make are a pain. The "test -s" catches obvious errors. info.html/%.html: info/%.t - perl $(srcdir)/info/emp2html.pl $< >$@ + $(call quiet-command,perl $(srcdir)/info/emp2html.pl $(info) <$< >$@,GEN $@) ### Explicit rules diff --git a/info/emp2html.pl b/info/emp2html.pl index 7b7d82e7..13069f93 100644 --- a/info/emp2html.pl +++ b/info/emp2html.pl @@ -31,9 +31,10 @@ # Drake Diedrich, 1996 # Markus Armbruster, 2004-2013 # -# Usage: emp2html.pl [INFO-FILE] +# Usage: emp2html.pl INFO... # -# Convert INFO-FILE (or else standard input) to HTML on standard output. +# Convert info source on standard input to HTML on standard output. +# INFO... are the info page names. use strict; use warnings; @@ -43,13 +44,18 @@ my $esc = "\\"; my $ignore = 0; my $is_subj; my @a; +my %topic; + +for (@ARGV) { + $topic{$_} = 1; +} print "\n"; print "\n"; print "
\n"; -line: while (<>) { +line: while (