diff options
| -rw-r--r-- | man/maintaining.texi | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/man/maintaining.texi b/man/maintaining.texi index c9e77ede2a1..988d5890b8c 100644 --- a/man/maintaining.texi +++ b/man/maintaining.texi | |||
| @@ -409,8 +409,8 @@ source files, and the tags file will still refer correctly to the source | |||
| 409 | files. If the tags file is in @file{/dev}, however, the file names are | 409 | files. If the tags file is in @file{/dev}, however, the file names are |
| 410 | made relative to the current working directory. This is useful, for | 410 | made relative to the current working directory. This is useful, for |
| 411 | example, when writing the tags to @file{/dev/stdout}. | 411 | example, when writing the tags to @file{/dev/stdout}. |
| 412 | 412 | ||
| 413 | When using a a relative file name, it should not be a symbolic link | 413 | When using a relative file name, it should not be a symbolic link |
| 414 | pointing to a tags file in a different directory, because this would | 414 | pointing to a tags file in a different directory, because this would |
| 415 | generally render the file names invalid. | 415 | generally render the file names invalid. |
| 416 | 416 | ||