Function dragEnd

tools/pythonauto/static/codemirrorepl/codemirrorepl.js:601–610

(e2)

                // Let the drag handler handle this.
                if (webkit) lineSpace.draggable = true;
                function dragEnd(e2) {
                    if (webkit) lineSpace.draggable = false;
                    draggingText = false;
                    up(); drop();
                    if (Math.abs(e.clientX - e2.clientX) + Math.abs(e.clientY - e2.clientY) < 10) {
                        e_preventDefault(e2);
                        setCursor(start.line, start.ch, true);
                        focusInput();
                    }
                }
                var up = connect(document, "mouseup", operation(dragEnd), true);
                var drop = connect(scroller, "drop", operation(dragEnd), true);
                draggingText = true;