From a95f7185d38c2b49ef50698211447e47b5be1558 Mon Sep 17 00:00:00 2001 From: Ben Gamari Date: Fri, 4 Oct 2019 14:25:26 -0400 Subject: doc: Write out documented flag list --- docs/users_guide/flags.py | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/docs/users_guide/flags.py b/docs/users_guide/flags.py index ac5de4cb57..90d6921827 100644 --- a/docs/users_guide/flags.py +++ b/docs/users_guide/flags.py @@ -53,6 +53,8 @@ from sphinx.errors import SphinxError from distutils.version import LooseVersion from utils import build_table_from_list +import os.path + ### Settings # Categories to titles as well as a canonical list of categories @@ -590,15 +592,23 @@ class ExtensionPrintDirective(Directive): ### Additional processing -# Convert every flagprint node into its output format def process_print_nodes(app, doctree, fromdocname): + # Convert every flagprint node into its output format for node in doctree.traverse(flagprint): node.generate_output(app, fromdocname) for node in doctree.traverse(extensionprint): node.generate_output(app, fromdocname) + # Write out file listing all documented flags + with open(os.path.join(app.outdir, 'ghc-flags.txt'), 'w') as f: + flag_names = \ + {name + for flag in app.env.all_flags + for name in flag['names']} + + f.write('\n'.join(flag_names)) # To avoid creating duplicates in the serialized environment, clear all # flags originating from a file before re-reading it. -- cgit v1.2.1