codemirror updated to 5.47.0

This commit is contained in:
zadam
2019-06-02 09:59:07 +02:00
parent e845b80e10
commit 54e37dea20
98 changed files with 10302 additions and 9881 deletions

View File

@@ -7,7 +7,7 @@
<link rel="stylesheet" href="../../lib/codemirror.css">
<script src="../../lib/codemirror.js"></script>
<script src="oz.js"></script>
<script type="text/javascript" src="../../addon/runmode/runmode.js"></script>
<script src="../../addon/runmode/runmode.js"></script>
<style>
.CodeMirror {border: 1px solid #aaa;}
</style>
@@ -49,7 +49,7 @@ end
</textarea>
<p>MIME type defined: <code>text/x-oz</code>.</p>
<script type="text/javascript">
<script>
var editor = CodeMirror.fromTextArea(document.getElementById("code"), {
lineNumbers: true,
mode: "text/x-oz",