diff --git a/docs/formal/fix-doxygen-unicode.py b/docs/formal/fix-doxygen-unicode.py
index 9b77b47c..90ec455d 100644
--- a/docs/formal/fix-doxygen-unicode.py
+++ b/docs/formal/fix-doxygen-unicode.py
@@ -115,6 +115,11 @@ def fix_line(line):
         else:
             for char, replacement in REPLACEMENTS:
                 part = part.replace(char, replacement)
+            # Replace any remaining non-ASCII with ? placeholder -- here, and
+            # not over the whole file, so that the protected tokens keep their
+            # Unicode: a \doxynewunicodechar{?} is an ASCII character, which
+            # newunicodechar refuses ("ASCII character requested").
+            part = part.encode('ascii', errors='replace').decode('ascii')
             result.append(part)
     return ''.join(result)
 
@@ -124,10 +129,8 @@ def fix_file(path):
     original = ''.join(lines)
     fixed_lines = [fix_line(l) for l in lines]
     content = ''.join(fixed_lines)
-    # Replace any remaining non-ASCII with ? placeholder
-    content = content.encode('ascii', errors='replace').decode('ascii')
     if content != original:
-        with open(path, 'w', encoding='ascii') as f:
+        with open(path, 'w', encoding='utf-8') as f:
             f.write(content)
         return True
     return False