diff options
Diffstat (limited to 'docs/users_guide/compare-flags.py')
| -rwxr-xr-x | docs/users_guide/compare-flags.py | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/docs/users_guide/compare-flags.py b/docs/users_guide/compare-flags.py index 5f0a1c9741..81a11b90e5 100755 --- a/docs/users_guide/compare-flags.py +++ b/docs/users_guide/compare-flags.py @@ -49,8 +49,8 @@ def read_documented_flags(doc_flags) -> Set[str]: def read_ghc_flags(ghc_path: str) -> Set[str]: ghc_output = subprocess.check_output([ghc_path, '--show-options']) - return {flag - for flag in ghc_output.decode('UTF-8').split('\n') + flags = {flag.strip() for flag in ghc_output.decode('UTF-8').split('\n')} + return {flag for flag in flags if not expected_undocumented(flag) if flag != ''} |