Tree-filter

An extension that allows you to filter by filename in the Jupyter notebook file tree (aka dashboard) page. Based on jdfreder/jupyter-tree-filter