From faef780f968bb1d8ea44c63e81d97a49e10aa188 Mon Sep 17 00:00:00 2001
From: Jordi Boggiano <j.boggiano@seld.be>
Date: Sun, 15 Jan 2012 18:05:43 +0100
Subject: [PATCH] Only show copy button in Opera since it does not support
 clipboard interaction from JS, fixes #3

---
 php-console.js | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/php-console.js b/php-console.js
index 995a43d..7e90037 100644
--- a/php-console.js
+++ b/php-console.js
@@ -95,7 +95,9 @@
 
         // events
         editor.getSession().selection.on('changeCursor', updateStatusBar);
-        editor.getSession().selection.on('changeSelection', prepareClippyButton);
+        if (window.navigator.userAgent.indexOf('Opera/') === 0) {
+            editor.getSession().selection.on('changeSelection', prepareClippyButton);
+        }
 
         // commands
         editor.commands.addCommand({