Put /dev into @file.

diff --git a/man/maintaining.texi b/man/maintaining.texi
index 7339d6a4f655b57e4370344dbdd6b6d4edd60ec7..e7d98e67591190ce624889e2f044394bc93eeb75 100644 (file)
--- a/man/maintaining.texi
+++ b/man/maintaining.texi
@@ -445,8 +445,8 @@ well as the files it directly contains.
 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