diff options
Diffstat (limited to 'lang/twelf/files/patch-twelf.info')
| -rw-r--r-- | lang/twelf/files/patch-twelf.info | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/lang/twelf/files/patch-twelf.info b/lang/twelf/files/patch-twelf.info new file mode 100644 index 000000000000..a74c22a58fce --- /dev/null +++ b/lang/twelf/files/patch-twelf.info @@ -0,0 +1,13 @@ +--- doc/info/twelf.info.orig Sat Jul 9 16:05:36 2005 ++++ doc/info/twelf.info Sat Jul 9 15:52:24 2005 +@@ -1,5 +1,10 @@ + This is twelf.info, produced by makeinfo version 4.2 from twelf.texi. + ++INFO-DIR-SECTION Programming ++START-INFO-DIR-ENTRY ++* Twelf User Guide: (twelf). The Twelf User's Guide. ++END-INFO-DIR-ENTRY ++ + + Indirect: + twelf.info-1: 71 |