diff options
| author | Gerd Moellmann <[email protected]> | 2000-06-20 19:54:37 +0000 |
|---|---|---|
| committer | Gerd Moellmann <[email protected]> | 2000-06-20 19:54:37 +0000 |
| commit | 0b634dc141e27ab7840e2b9a7d3753f838f432e0 (patch) | |
| tree | 89ba13ab18f99a5c537d820f6409f5443512aa87 /man | |
| parent | ce0b67174f75fcdf0c57a7bfdb80368360f27217 (diff) | |
@setfilename to ../info/reftex.
Diffstat (limited to 'man')
| -rw-r--r-- | man/reftex.texi | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/man/reftex.texi b/man/reftex.texi index f7cb412493..cff1f4a19e 100644 --- a/man/reftex.texi +++ b/man/reftex.texi @@ -1,6 +1,6 @@ \input texinfo @c -*-texinfo-*- @c %**start of header -@setfilename ../reftex +@setfilename ../info/reftex @settitle RefTeX User Manual @dircategory Editors @direntry |