Make the delays configurable in settings.js

1 files changed, 8 insertions, 12 deletions

diff --git a/js/auto-reload.js b/js/auto-reload.js
index 3159bfd1..fa856bd9 100644
--- a/js/auto-reload.js
+++ b/js/auto-reload.js
@@ -27,20 +27,16 @@ $(document).ready(function(){
 	
 	var poll_interval;
 
-	// number of ms to wait before reloading
-	var poll_interval_delay;
-
-	// If at the bottom of the page, reload more quickly.
-	var poll_interval_mindelay_bottom = 3000;
-	var poll_interval_mindelay_top    = 10000;
 
-	poll_interval_delay = poll_interval_mindelay_bottom;
+	// Grab the settings
+	var settings = new script_settings('auto-reload');
+	var poll_interval_mindelay_bottom = settings.get('min_delay_bottom', 3000);
+	var poll_interval_mindelay_top    = settings.get('min_delay_top', 10000);
+	var poll_interval_maxdelay        = settings.get('max_delay', 600000);
+	var poll_interval_shortdelay      = settings.get('quick_delay', 100);
 
-	// Don't take longer than this to reload.
-	var poll_interval_maxdelay = 600000;
-
-	// Upon scrolling to the bottom, reload very quickly.
-	var poll_interval_shortdelay = 100;
+	// number of ms to wait before reloading
+	var poll_interval_delay = poll_interval_mindelay_bottom;
 
 	var end_of_page = false;