From d7a3e415d58e746e19ddd7e1f03e792ac2f0ddf8 Mon Sep 17 00:00:00 2001
From: Jakub Vrana <jakub@vrana.cz>
Date: Mon, 3 Jan 2011 16:42:08 +0100
Subject: [PATCH] Don't use AJAX with Alt

---
 adminer/static/functions.js | 7 +++----
 editor/static/editing.js    | 2 +-
 2 files changed, 4 insertions(+), 5 deletions(-)

diff --git a/adminer/static/functions.js b/adminer/static/functions.js
index 9307f0f0..ce306153 100644
--- a/adminer/static/functions.js
+++ b/adminer/static/functions.js
@@ -191,7 +191,7 @@ function ajax(url, callback, data) {
 			xmlhttp.setRequestHeader('Content-Type', 'application/x-www-form-urlencoded');
 		}
 		xmlhttp.setRequestHeader('X-Requested-With', 'XMLHttpRequest');
-		xmlhttp.onreadystatechange = function (text) {
+		xmlhttp.onreadystatechange = function () {
 			if (xmlhttp.readyState == 4) {
 				var redirect = xmlhttp.getResponseHeader('X-AJAX-Redirect');
 				if (redirect && history.replaceState) {
@@ -222,8 +222,7 @@ function ajaxSetHtml(url) {
 	});
 }
 
-var ajaxState = 0;
-var ajaxTimeout;
+var ajaxState = 0, ajaxTimeout;
 
 /** Safely load content to #content
 * @param string
@@ -279,7 +278,7 @@ function ajaxSend(url, data) {
 * @return XMLHttpRequest or false in case of an error
 */
 function ajaxMain(url, data, event) {
-	if (!history.pushState || (event && (event.ctrlKey || event.shiftKey || event.metaKey))) {
+	if (!history.pushState || (event && (event.ctrlKey || event.shiftKey || event.altKey || event.metaKey))) {
 		return false;
 	}
 	history.pushState(data, '', url);
diff --git a/editor/static/editing.js b/editor/static/editing.js
index 70998ba6..b49666b2 100644
--- a/editor/static/editing.js
+++ b/editor/static/editing.js
@@ -1,4 +1,4 @@
 // Editor specific functions
 
-function bodyLoad(version) {
+function bodyLoad(version, protocol) {
 }