diff -r 4ade0d387429 -r 1c0a6a957114 etc/options
--- a/etc/options	Tue Dec 12 18:53:40 2017 +0100
+++ b/etc/options	Wed Dec 13 16:18:40 2017 +0100
@@ -13,8 +13,6 @@
   -- "alternative document variants (separated by colons)"
 option document_tags : string = ""
   -- "default command tags (separated by commas)"
-option document_positions : bool = true
-  -- "inline original source positions into generated tex files"
 
 option thy_output_display : bool = false
   -- "indicate output as multi-line display-style material"