Merge branch 'maint'

diff --git a/Documentation/Makefile b/Documentation/Makefile
index e82596dcdf0545d528806797c990e101d40f1436..a637d8d559b6a41505e5381b92d523e55f4b3be8 100644 (file)
--- a/Documentation/Makefile
+++ b/Documentation/Makefile
@@ -90,14 +90,17 @@ cmds_txt = cmds-ancillaryinterrogators.txt \
        cmds-purehelpers.txt \
        cmds-foreignscminterface.txt
 
-$(cmds_txt): cmd-list.perl $(MAN1_TXT)
+$(cmds_txt): cmd-list.made
+
+cmd-list.made: cmd-list.perl $(MAN1_TXT)
        perl ./cmd-list.perl
+       date >$@
 
 git.7 git.html: git.txt core-intro.txt
 
 clean:
        rm -f *.xml *.xml+ *.html *.html+ *.1 *.7 howto-index.txt howto/*.html doc.dep
-       rm -f $(cmds_txt)
+       rm -f $(cmds_txt) *.made
 
 %.html : %.txt
        rm -f $@+ $@