add back the whietspace character that we eat

wesleywright · wesleywright · commit fb2f37c6ca6d · 2025-02-05T14:35:10.000Z
diff --git a/misc/gen_blog_post_html.py b/misc/gen_blog_post_html.py
@@ -128,7 +128,7 @@ def convert(src: str) -> str:
     )
     # Note the leading space to avoid stomping on strings that contain #\d in the middle (such as
     # links to PRs in other repos)
-    h = re.sub(r" #([0-9]+)", r'PR <a href="https://github.com/python/mypy/pull/\1">\1</a>', h)
+    h = re.sub(r" #([0-9]+)", r' PR <a href="https://github.com/python/mypy/pull/\1">\1</a>', h)
     h = re.sub(r"\) \(PR", ", PR", h)
 
     # Markdown links

Original file line number	Diff line number	Diff line change
`@@ -128,7 +128,7 @@ def convert(src: str) -> str:`
`128`	`128`	`)`
`129`	`129`	`# Note the leading space to avoid stomping on strings that contain #\d in the middle (such as`
`130`	`130`	`# links to PRs in other repos)`
`131`		`- h = re.sub(r" #([0-9]+)", r'PR <a href="https://github.com/python/mypy/pull/\1">\1</a>', h)`
	`131`	`+ h = re.sub(r" #([0-9]+)", r' PR <a href="https://github.com/python/mypy/pull/\1">\1</a>', h)`
`132`	`132`	`h = re.sub(r"\) \(PR", ", PR", h)`
`133`	`133`
`134`	`134`	`# Markdown links`