From 8d5c12dfac0f5f297872f7d63ea19397d5ce8f6f Mon Sep 17 00:00:00 2001 From: Jeremy Tuloup Date: Fri, 15 Jan 2021 14:45:01 +0100 Subject: [PATCH] Add the codemirror singleton plugin --- builder/index.js | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/builder/index.js b/builder/index.js index 17d3a1e93..b817e9fb8 100644 --- a/builder/index.js +++ b/builder/index.js @@ -88,7 +88,10 @@ async function main() { ].includes(id) ), require('@jupyterlab/codemirror-extension').default.filter(({ id }) => - ['@jupyterlab/codemirror-extension:services'].includes(id) + [ + '@jupyterlab/codemirror-extension:services', + '@jupyterlab/codemirror-extension:codemirror' + ].includes(id) ), require('@jupyterlab/completer-extension').default.filter(({ id }) => ['@jupyterlab/completer-extension:manager'].includes(id)