Change some node names and clean up the menu.
authorrms <rms>
Fri, 15 May 1992 18:37:50 +0000 (18:37 +0000)
committerrms <rms>
Fri, 15 May 1992 18:37:50 +0000 (18:37 +0000)
commit816ff5a2ff814553569ebc732ad023a17a9f9466
tree91cc7f39869b7ac046554f1b67ef2dca5b4d4ee4
parent04771a3c8bd7e4bb7dc72d4e0a9a42b633881ac8
Change some node names and clean up the menu.
manual/setjmp.texi