From 6357d3f74da31e4f08ae244decfb55ef8300831e Mon Sep 17 00:00:00 2001
From: Jeremy Tuloup <jeremy.tuloup@gmail.com>
Date: Sun, 3 Apr 2022 18:41:00 +0200
Subject: [PATCH] Include codemirror commands plugin in edit

---
 app/index.js | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/app/index.js b/app/index.js
index 8e1864cdc..954deefd0 100644
--- a/app/index.js
+++ b/app/index.js
@@ -196,6 +196,9 @@ async function main() {
     }
     case 'edit': {
       baseMods = baseMods.concat([
+        require('@jupyterlab/codemirror-extension').default.filter(({ id }) =>
+          ['@jupyterlab/codemirror-extension:commands'].includes(id)
+        ),
         require('@jupyterlab/fileeditor-extension').default.filter(({ id }) =>
           ['@jupyterlab/fileeditor-extension:completer'].includes(id)
         ),