New text notebook menu in Jupyter Notebook#525

Merged

mwouts merged 4 commits intomasterfrom new_text_notebook

May 28, 2020

+123-7

Commits on May 26, 2020

Use jupytext.js rather than index.js for the Jupyter Notebook extension
mwouts
committed

Commits on May 27, 2020

New Text Notebook menu (WIP)
mwouts
committed

Commits on May 28, 2020