##// END OF EJS Templates
added new use_shortcut method to shortcuts...
added new use_shortcut method to shortcuts this way, you can ask if a particular event will be handled by the shortcuts system. This takes away the need to special-case many different possible keys which should be ignored by codemirror by ignoring them en masse.

File last commit:

r12098:20cd990c
r15758:1ebe52ee
Show More
htmlnotebook.html
9 lines | 263 B | text/html | HtmlLexer
<html>
<head>
<meta http-equiv="Refresh" content="0; url=notebook.html" />
<title>Notebook page has move</title>
</head>
<body>
<p>The notebook page has moved to <a href="notebook.html">this link</a>.</p>
</body>
</html>