[paste] Fix #2384 and #1883

As described in the comment, there was actually an intermediate selection being created, which clobbered the middle-click paste buffer and thus resulted in a $ being pasted instead of the actual content the user wanted. It's still a mystery why you couldn't repro it, but my guess is that due to some configuration (maybe in your window manager) your system wasn't updating the paste buffer as eagerly as Debian and Unity do by default.

Author: mtaran-google

lib/codemirror.js

@@ -2452,8 +2452,12 @@
       if (webkit && !cm.state.fakedLastChar && !(new Date - cm.state.lastMiddleDown < 200)) {
         var start = d.input.selectionStart, end = d.input.selectionEnd;
         d.input.value += "$";
-        d.input.selectionStart = start;
+        // The selection end needs to be set before the start, otherwise there
+        // can be an intermediate non-empty selection between the two, which
+        // can override the middle-click paste buffer on linux and cause the
+        // wrong thing to get pasted.
         d.input.selectionEnd = end;
+        d.input.selectionStart = start;
         cm.state.fakedLastChar = true;
       }
       cm.state.pasteIncoming = true;