From efe34eb48ad14138ad5be7191ef9485ab5224462 Mon Sep 17 00:00:00 2001
From: Jeremy Tuloup <jeremy.tuloup@gmail.com>
Date: Thu, 27 Jan 2022 10:53:59 +0100
Subject: [PATCH] Add `@jupyterlab/notebook-extension:export` plugin

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

diff --git a/app/index.js b/app/index.js
index 7e6d972cb..5fd3d23eb 100644
--- a/app/index.js
+++ b/app/index.js
@@ -120,6 +120,7 @@ async function main() {
     require('@jupyterlab/notebook-extension').default.filter(({ id }) =>
       [
         '@jupyterlab/notebook-extension:code-console',
+        '@jupyterlab/notebook-extension:export',
         '@jupyterlab/notebook-extension:factory',
         '@jupyterlab/notebook-extension:tracker',
         '@jupyterlab/notebook-extension:widget-factory'