trying to get reload button on gruntose working again.

diff --git a/webby/javascript/gruntose/launchers.js b/webby/javascript/gruntose/launchers.js
index 08723dd72045761eac8555530b170d3086d58dc1..9349ad3a5c81562c127f0f026f6fd5d422b088a8 100644 (file)
--- a/webby/javascript/gruntose/launchers.js
+++ b/webby/javascript/gruntose/launchers.js
@@ -9,7 +9,8 @@
 ////////////////////////////////////////////////////////////////////////////
 
 function jump_appropriate() {
-  window.location.reload(true);
+//stopped working:  window.location.reload(true);
+  window.location = window.location;
 }
 
 function jump_to_anchor(anchor) {