CI: detect & remove multiline verbatim blocks

scripts/extract-comments.py

@@ -6,6 +6,7 @@ import os
 import re
 
 INLINE_CODE_RE = re.compile(r'\[[^]]*?\]')
+VERBATIM_RE = re.compile(r'<<.*?>>')
 
 def comment_ranges(src):
     "Identify comments in Coq .v files."
@@ -41,8 +42,10 @@ def process(opts, fname):
     out = sys.stdout
     for (a, b) in comment_ranges(src):
         txt = src[a:b]
-        print(INLINE_CODE_RE.sub('', txt))
-#     out.close()
+        txt = txt.replace('\n', ' ')
+        txt = VERBATIM_RE.sub('', txt)
+        txt = INLINE_CODE_RE.sub('', txt)
+        print(txt)
 
 def parse_args():
     parser = argparse.ArgumentParser(

scripts/flag-typos-in-comments.sh

@@ -10,7 +10,6 @@ do
 
 	#Here, sed is used to remove verbatim text (enclosed in <<>>)
 	for WORD in $(scripts/extract-comments.py "$SRC" \
-		| sed 's/<<.*>>//g' \
 		| hunspell -p $KNOWN_EXCEPTIONS -l -d en_US \
 		| sort \
 		| uniq)