Fix `Details' menu item.
authorrms <rms>
Wed, 23 Sep 1992 04:36:24 +0000 (04:36 +0000)
committerrms <rms>
Wed, 23 Sep 1992 04:36:24 +0000 (04:36 +0000)
commitad3edf132d40ded5d6246a971cd959d72dca466d
treed9a7a0c059994544f41f58c92901c98856fe1405
parent6e5a72a10f69aaef878aee64581e891ae43920ef
Fix `Details' menu item.
manual/setjmp.texi