Add manager plugin

4 years ago · 2e1a6c2684
parent ac8ede6dea
commit 2e1a6c2684
1 changed files with 2 additions and 1 deletions
--- a/app/index.js
+++ b/app/index.js
@ -112,7 +112,8 @@ async function main() {
    require('@jupyterlab/docmanager-extension').default.filter(({ id }) =>
      [
        '@jupyterlab/docmanager-extension:plugin',
-        '@jupyterlab/docmanager-extension:download'
+        '@jupyterlab/docmanager-extension:download',
+        '@jupyterlab/docmanager-extension:manager'
      ].includes(id)
    ),
    require('@jupyterlab/docprovider-extension'),