Function removeGutterMarker

tools/pythonauto/static/codemirrorepl/codemirrorepl.js:1676–1680

(line)

            return line;
        }
        function removeGutterMarker(line) {
            if (typeof line == "number") line = getLine(clipLine(line));
            line.gutterMarker = null;
            gutterDirty = true;
        }

        function changeLine(handle, op) {
            var no = handle, line = handle;