changeset 57102:5c078eb058f8

Put /dev into @file.
author Francesco Potortì <pot@gnu.org>
date Tue, 14 Sep 2004 15:22:48 +0000
parents 8f78d0e23932
children ed7a08ddfaf8
files man/maintaining.texi
diffstat 1 files changed, 2 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/man/maintaining.texi	Tue Sep 14 11:12:00 2004 +0000
+++ b/man/maintaining.texi	Tue Sep 14 15:22:48 2004 +0000
@@ -445,8 +445,8 @@
 directory where the tags file was initially written.  This way, you can
 move an entire directory tree containing both the tags file and the
 source files, and the tags file will still refer correctly to the source
-files.  If the tags file is in /dev, however, the file names are made
-relative to the current working directory.
+files.  If the tags file is in @file{/dev}, however, the file names are
+made relative to the current working directory.
 
   If you specify absolute file names as arguments to @code{etags}, then
 the tags file will contain absolute file names.  This way, the tags file