diff options
Diffstat (limited to 'src/options/builtin_options.toml')
| -rw-r--r-- | src/options/builtin_options.toml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/options/builtin_options.toml b/src/options/builtin_options.toml index 6ef79cd0b..b5f2ed593 100644 --- a/src/options/builtin_options.toml +++ b/src/options/builtin_options.toml @@ -1,3 +1,3 @@ id = "BUILTIN" name = "Builtin theory" -header = "options/builtin_options.h" + |