codemirror/CodeMirror — pull request #2891 by mihailik (2014-10-25 00:39:23+00:00)
Title: Mouse selection on Android.

Android devices allow physical mice, but web pages tend to treat mouse as a precise touch device.

This patch makes CodeMirror treat mouse click-drag as a normal selection, whilst still keeping touch click-drag for panning.

Tested on Android:
* Chrome Mobile,
* Built-in browser (on 4.4, still need to try on older Webkits),
* FireFox,
* Opera
* Opera Classic
It works totally as expected. Mouse selects, touching pans.

Tested on Windows 8+touchscreen:
* Chrome,
* IE
Works half-way: Chrome selects with both mouse and single-finger touch, pans with multi-finger touch; IE always pans.

Use the standard demo pages for quick testing:

http://mihailik.github.io/CodeMirror/demo/folding.html
http://mihailik.github.io/CodeMirror/demo/buffers.html