Docs xrefs checking: ignore refs that should be internal @ref

Some docs which contains @ruser instances are used in both the
Internals Reference and the Notation Reference, so they cannot be
replaced with @ref.

diff --git a/buildscripts/check_texi_refs.py b/buildscripts/check_texi_refs.py
index 4508baa5605f163519da8e7601854774e8af15b5..dff7e334f1ccc45d9e2ab039ef8b222ef8443a48 100755 (executable)
--- a/buildscripts/check_texi_refs.py
+++ b/buildscripts/check_texi_refs.py
@@ -361,9 +361,9 @@ not followed by punctuation\n" % (file, line, name))
     new_name = name
 
     if type != 'ref' and type == manual and not commented_out:
-        fixed = False
-        bad_ref = True
         if useful_fix:
+            fixed = False
+            bad_ref = True
             stdout.write ("\n%s: %d: `%s': external %s x-ref should be internal\n"
                           % (file, line, name, type))
             if options.auto_fix or yes_prompt ("Fix this?"):