etc/options
changeset 70801 5352449209b1
parent 70800 44eeca528557
child 70914 05c4c6a99b3f
--- a/etc/options	Mon Oct 07 17:20:26 2019 +0200
+++ b/etc/options	Mon Oct 07 21:51:31 2019 +0200
@@ -222,7 +222,7 @@
 option headless_commit_cleanup_delay : real = 60
   -- "delay for cleanup of already imported theories (seconds, 0 = disabled)"
 
-option headless_load_limit : int = 5
+option headless_load_limit : real = 5.0
   -- "limit in MB for loaded theory files (0 = unlimited)"