summaryrefslogtreecommitdiff
path: root/src/options/sets_options.toml
diff options
context:
space:
mode:
Diffstat (limited to 'src/options/sets_options.toml')
-rw-r--r--src/options/sets_options.toml1
1 files changed, 0 insertions, 1 deletions
diff --git a/src/options/sets_options.toml b/src/options/sets_options.toml
index 0f206f980..db9cfa480 100644
--- a/src/options/sets_options.toml
+++ b/src/options/sets_options.toml
@@ -1,6 +1,5 @@
id = "SETS"
name = "Sets"
-header = "options/sets_options.h"
[[option]]
name = "setsProxyLemmas"
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback