summaryrefslogtreecommitdiff
path: root/src/options/parser_options.toml
diff options
context:
space:
mode:
authorAndres Noetzli <andres.noetzli@gmail.com>2020-04-02 11:59:34 -0700
committerGitHub <noreply@github.com>2020-04-02 13:59:34 -0500
commite24e6f3620996ee9e5010d30fefc51247cc55fdc (patch)
treecb44e6cd092956a05ac00d4104d19bd0e1f36eb4 /src/options/parser_options.toml
parentaa6fb6fa3df0b1519e6763e72541c022396ab1dc (diff)
Remove undocumented/uncommon aliases (#4177)
This commit removes aliases that are either undocumented or associated with uncommon options. Note: The removal of --statistics, --language, and --output-language may be controversial. The options were undocumented previously and I am in favor of simplifying the options as much as possible, however. Please let me know what you think.
Diffstat (limited to 'src/options/parser_options.toml')
-rw-r--r--src/options/parser_options.toml10
1 files changed, 0 insertions, 10 deletions
diff --git a/src/options/parser_options.toml b/src/options/parser_options.toml
index 71074d420..72c7b51a0 100644
--- a/src/options/parser_options.toml
+++ b/src/options/parser_options.toml
@@ -27,11 +27,6 @@ header = "options/parser_options.h"
read_only = true
help = "disable ALL semantic checks, including type checks"
-[[alias]]
- category = "undocumented"
- long = "no-checking"
- links = ["--no-type-checking"]
-
[[option]]
name = "globalDeclarations"
smt_name = "global-declarations"
@@ -61,11 +56,6 @@ header = "options/parser_options.h"
default = "true"
read_only = true
-[[alias]]
- category = "undocumented"
- long = "no-include-file"
- links = ["--no-filesystem-access"]
-
[[option]]
name = "forceLogicString"
smt_name = "force-logic"
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback