diff options
-rw-r--r-- | doc/develenv/ChangeLog | 4 | ||||
-rw-r--r-- | doc/develenv/develenv.texi | 2 |
2 files changed, 5 insertions, 1 deletions
diff --git a/doc/develenv/ChangeLog b/doc/develenv/ChangeLog index c7aeec1861..69c6309e84 100644 --- a/doc/develenv/ChangeLog +++ b/doc/develenv/ChangeLog @@ -1,3 +1,7 @@ +2003-04-29 Ralf Corsepius <corsepiu@faw.uni-ulm.de> + + * develenv.texi: Fix @setfilename to develenv.info. + 2003-04-16 Joel Sherrill <joel@OARcorp.com> * Makefile.am, develenv.texi: Remove unused file. diff --git a/doc/develenv/develenv.texi b/doc/develenv/develenv.texi index 76cd365a5e..47fba4168c 100644 --- a/doc/develenv/develenv.texi +++ b/doc/develenv/develenv.texi @@ -1,6 +1,6 @@ \input texinfo @c -*-texinfo-*- @c %**start of header -@setfilename develenv +@setfilename develenv.info @setcontentsaftertitlepage @syncodeindex vr fn @synindex ky cp |