From c18db44fd7a666c17c60769db57a4e23e64bc7ea Mon Sep 17 00:00:00 2001
From: Thierry Parmentelat <thierry.parmentelat@inria.fr>
Date: Tue, 3 Dec 2013 14:43:11 +0100
Subject: [PATCH] miscell cosmetic

---
 .gitignore                                 | 1 +
 Makefile                                   | 2 +-
 manifold/static/js/manifold.js             | 2 +-
 plugins/querytable/static/js/querytable.js | 2 +-
 plugins/tabs/static/js/tabs.js             | 1 -
 5 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/.gitignore b/.gitignore
index ed36fe74..52c5d5fe 100644
--- a/.gitignore
+++ b/.gitignore
@@ -15,3 +15,4 @@ build/
 plugins/*/*.css
 plugins/*/*.js
 plugins/*/*.html
+myslice.ini*
diff --git a/Makefile b/Makefile
index e3449bbd..ad27d395 100644
--- a/Makefile
+++ b/Makefile
@@ -91,7 +91,7 @@ redo-templates: clean-templates templates
 #################### compute emacs tags
 # list files under git but exclude third-party stuff like bootstrap and jquery
 myfiles: force
-	@git ls-files | egrep -v 'insert(_|-)above|third-party/|play/'
+	@git ls-files | egrep -v 'insert(_|-)above|third-party/|to-be-integrated/'
 
 # in general it's right to rely on the contents as reported by git
 tags: force
diff --git a/manifold/static/js/manifold.js b/manifold/static/js/manifold.js
index e4b7db9b..1bb5b975 100644
--- a/manifold/static/js/manifold.js
+++ b/manifold/static/js/manifold.js
@@ -356,7 +356,7 @@ var manifold = {
             var publish_uuid=tuple.publish_uuid;
             // by default we publish using the same uuid of course
             if (publish_uuid==undefined) publish_uuid=query.query_uuid;
-            if (manifold.asynchroneous_debug) {
+            if (manifold.publish_result_debug) {
                 messages.debug("sending POST on " + manifold.proxy_url + query.__repr());
             }
 
diff --git a/plugins/querytable/static/js/querytable.js b/plugins/querytable/static/js/querytable.js
index 772ff7e0..42dfee5e 100644
--- a/plugins/querytable/static/js/querytable.js
+++ b/plugins/querytable/static/js/querytable.js
@@ -7,7 +7,7 @@
 (function($) {
 
     var debug=false;
-    debug=true
+//    debug=true
 
     var QueryTable = Plugin.extend({
 
diff --git a/plugins/tabs/static/js/tabs.js b/plugins/tabs/static/js/tabs.js
index 4612dd25..f9cd2a7c 100644
--- a/plugins/tabs/static/js/tabs.js
+++ b/plugins/tabs/static/js/tabs.js
@@ -33,7 +33,6 @@ var tabs_helper = {
 	if (tabs_helper.debug) messages.debug ("setting active for " + domid + " to active_domid=" + active_domid);
 	// build something like "#uldomid a[href='#active_domid']"
 	var selector="#"+domid+" a[href='#"+active_domid+"']";
-	console.log("selector="+selector);
 	$(selector).tab('show');
     },
     set_from_saved_active_domid : function (domid) {
-- 
2.43.0