diff options
| author | Glenn Morris <rgm@gnu.org> | 2016-08-15 12:48:01 -0400 |
|---|---|---|
| committer | Glenn Morris <rgm@gnu.org> | 2016-08-15 12:48:01 -0400 |
| commit | 126f95a708d637941e9eae1b023a87733bb5fd38 (patch) | |
| tree | 4afc50ad8b59e36e8d97f028fbec4439490b0a1b /doc | |
| parent | 15c16a5d3b45c95bcb0855b607f975310a707ee1 (diff) | |
* doc/misc/tramp.texi: Adapt 2016-08-14 change for makeinfo 4.
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/misc/tramp.texi | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/misc/tramp.texi b/doc/misc/tramp.texi index d64d5e5eba..5e04a2d5a2 100644 --- a/doc/misc/tramp.texi +++ b/doc/misc/tramp.texi @@ -65,8 +65,8 @@ copy and modify this GNU manual.'' @contents -@node Top, Overview, (dir), (dir) @ifnottex +@node Top, Overview, (dir), (dir) @top @value{tramp} version @value{trampver} User Manual This file documents @value{tramp} version @value{trampver}, a remote file |