From 5b99456210d1e57ad94e04f182d10083c47df446 Mon Sep 17 00:00:00 2001
From: Mikolaj Rybinski <mikolaj.rybinski@id.ethz.ch>
Date: Fri, 17 Sep 2021 16:03:35 +0200
Subject: [PATCH] In .binder/postBuild: don't store timing in notebooks
metadata
---
binder/postBuild | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/binder/postBuild b/binder/postBuild
index 9bf0873..774fd2a 100755
--- a/binder/postBuild
+++ b/binder/postBuild
@@ -13,4 +13,4 @@ jupyter serverextension enable --py jupyter_lsp --sys-prefix
npm cache clean --force
mkdir -p ~/.jupyter/lab/user-settings/@jupyterlab/notebook-extension/
-echo '{"codeCellConfig": {"lineNumbers": true}, "recordTiming": true}' > ~/.jupyter/lab/user-settings/@jupyterlab/notebook-extension/tracker.jupyterlab-settings
+echo '{"codeCellConfig": {"lineNumbers": true}, "recordTiming": false}' > ~/.jupyter/lab/user-settings/@jupyterlab/notebook-extension/tracker.jupyterlab-settings
--
GitLab