diff -r 0484086194ce -r 9171d1ce5a35 etc/options
--- a/etc/options	Thu Jan 03 21:04:16 2019 +0100
+++ b/etc/options	Thu Jan 03 21:06:39 2019 +0100
@@ -277,6 +277,12 @@
 option export_theory : bool = false
 
 
+section "Theory update"
+
+option update_mixfix_cartouches : bool = false
+  -- "update mixfix templates to use cartouches instead of double quotes"
+
+
 section "Build Database"
 
 option build_database_server : bool = false