diff options
Diffstat (limited to 'docs/users_guide/conf.py')
| -rw-r--r-- | docs/users_guide/conf.py | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/docs/users_guide/conf.py b/docs/users_guide/conf.py index eb81cf51ec..6fd94db74f 100644 --- a/docs/users_guide/conf.py +++ b/docs/users_guide/conf.py @@ -36,10 +36,6 @@ nitpick_ignore = [ ("c:type", "bool"), - # See #17314 - ("ghc-flag", "-pgmo ⟨port⟩"), - ("ghc-flag", "-pgmo ⟨option⟩"), - ("extension", "DoAndIfThenElse"), ("extension", "RelaxedPolyRec"), |