* doc/misc/tramp.texi: Adapt 2016-08-14 change for makeinfo 4.
commit126f95a708d637941e9eae1b023a87733bb5fd38
authorGlenn Morris <rgm@gnu.org>
Mon, 15 Aug 2016 16:48:01 +0000 (15 12:48 -0400)
committerGlenn Morris <rgm@gnu.org>
Mon, 15 Aug 2016 16:48:01 +0000 (15 12:48 -0400)
tree4afc50ad8b59e36e8d97f028fbec4439490b0a1b
parent15c16a5d3b45c95bcb0855b607f975310a707ee1
* doc/misc/tramp.texi: Adapt 2016-08-14 change for makeinfo 4.
doc/misc/tramp.texi