diff options
Diffstat (limited to 'Utilities/Sphinx/create_identifiers.py')
-rwxr-xr-x | Utilities/Sphinx/create_identifiers.py | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/Utilities/Sphinx/create_identifiers.py b/Utilities/Sphinx/create_identifiers.py index 4513434..e638950 100755 --- a/Utilities/Sphinx/create_identifiers.py +++ b/Utilities/Sphinx/create_identifiers.py @@ -21,6 +21,7 @@ newlines = [] for line in lines: mapping = (("command", "command"), + ("envvar", "envvar"), ("variable", "variable"), ("generator", "generator"), ("target property", "prop_tgt"), |