diff options
Diffstat (limited to 'Build/source/texk/web2c/man/Makefile.in')
-rw-r--r-- | Build/source/texk/web2c/man/Makefile.in | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/Build/source/texk/web2c/man/Makefile.in b/Build/source/texk/web2c/man/Makefile.in index 1bc76119302..193137c1e64 100644 --- a/Build/source/texk/web2c/man/Makefile.in +++ b/Build/source/texk/web2c/man/Makefile.in @@ -468,7 +468,8 @@ EXTRA_DIST = $(bootstrap_man_sources) $(web_man_sources) tex.man \ bootstrap_man_sources = ctie.man cweb.man ctwill.man tangle.man tie.man # Symlinks within $(man1dir): FILE:LINK indicates LINK.1->FILE.1 -man1_links = cweb:ctangle cweb:cweave ctwill:ctwill-refsort \ +man1_links = cweb:ctangle cweb:cweave \ + ctwill:ctwill-proofsort ctwill:ctwill-refsort \ ctwill:ctwill-twinx twill:twill-refsort $(am__append_3) \ $(am__append_5) $(am__append_6) $(am__append_10) \ $(am__append_12) $(am__append_14) $(am__append_17) \ |