summaryrefslogtreecommitdiff
path: root/src/options/options.h
diff options
context:
space:
mode:
authorMathias Preiner <mathias.preiner@gmail.com>2019-12-17 13:43:44 -0800
committerGitHub <noreply@github.com>2019-12-17 13:43:44 -0800
commite9499c41f405df8b42fd9ae10004b1b91a869106 (patch)
treefa1475f43a3e61b8f6ffdcb903b65919eba28661 /src/options/options.h
parent9b2914ed9f7b14ecf535ffe9e1328d0fa042e072 (diff)
Generate code for options with modes. (#3561)
This commit adds support for code generation of options with modes (enums). From now on option enums can be specified in the corresponding *.toml files without the need of extra code. All option enums are now in the options namespace.
Diffstat (limited to 'src/options/options.h')
-rw-r--r--src/options/options.h2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/options/options.h b/src/options/options.h
index c321b3499..1493ceac9 100644
--- a/src/options/options.h
+++ b/src/options/options.h
@@ -195,7 +195,7 @@ public:
// Get accessor functions.
InputLanguage getInputLanguage() const;
- InstFormatMode getInstFormatMode() const;
+ options::InstFormatMode getInstFormatMode() const;
OutputLanguage getOutputLanguage() const;
bool getUfHo() const;
bool getCheckProofs() const;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback