From e614a39e0183c37b4b4a2bd14e33ae478f844b3a Mon Sep 17 00:00:00 2001 From: Jeremy Tuloup Date: Mon, 20 Sep 2021 15:55:25 +0200 Subject: [PATCH] Expose the file editor plugin to all pages --- app/index.js | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/app/index.js b/app/index.js index 14a70820b..f540e2c49 100644 --- a/app/index.js +++ b/app/index.js @@ -122,6 +122,9 @@ async function main() { ['@jupyterlab/docmanager-extension:plugin'].includes(id) ), require('@jupyterlab/docprovider-extension'), + require('@jupyterlab/fileeditor-extension').default.filter(({ id }) => + ['@jupyterlab/fileeditor-extension:plugin'].includes(id) + ), require('@jupyterlab/mainmenu-extension'), require('@jupyterlab/mathjax2-extension'), require('@jupyterlab/notebook-extension').default.filter(({ id }) => @@ -196,9 +199,6 @@ async function main() { require('@jupyterlab/completer-extension').default.filter(({ id }) => ['@jupyterlab/completer-extension:files'].includes(id) ), - require('@jupyterlab/fileeditor-extension').default.filter(({ id }) => - ['@jupyterlab/fileeditor-extension:plugin'].includes(id) - ), require('@jupyterlab/filebrowser-extension').default.filter(({ id }) => [ '@jupyterlab/filebrowser-extension:browser',