diff options
Diffstat (limited to 'doc/misc/sem-user.texi')
| -rw-r--r-- | doc/misc/sem-user.texi | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/doc/misc/sem-user.texi b/doc/misc/sem-user.texi index f986c0fd452..ec35b92d61f 100644 --- a/doc/misc/sem-user.texi +++ b/doc/misc/sem-user.texi @@ -1330,7 +1330,3 @@ To add other kind of decorations on a tag, @code{NAME-highlight} must use @dfn{semantic-decorate-tag}, and other functions of the semantic decoration @var{api} found in this library. @end defun - -@ignore - arch-tag: 760dca58-7119-484e-8237-866cbaf36f79 -@end ignore |