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)
manual/setjmp.texi

index fd384b4..2f6596e 100644 (file)
@@ -11,7 +11,7 @@ functions.
 
 @menu
 * Intro: Non-Local Intro.        When and how to use these facilities.
-* Details: Non-Local Details::   Functions for nonlocal exits.
+* Details: Non-Local Details.   Functions for nonlocal exits.
 * Non-Local Exits and Signals::  Portability issues.
 @end menu