How to copy a file locally?

[beenje]

The extension is really nice to run a notebook directly from a GitHub repository.

I think a common use case is to create a local copy of a notebook so that it can be modified and saved locally. I can't find an easy way to copy a file from the GitHub drive to the local filesystem.

I tried to use "Copy" from the contextual menu (when right clicking on a file) and then "Paste" but nothing happens.

The only way I found so far is to open the notebook in a text editor, copy the content, create a text file, paste, and rename the file. Not super user friendly. Is there a better way to do that?

[ian-r-rose]

Sorry for the slow response @beenje.

Copy/Paste of files between different filebrowsers should be possible to implement, but it has not been yet (I would love to see someone take a crack it it! :)). The relevant functionality to implement would be here: https://github.com/jupyterlab/jupyterlab/blob/cbb227840b764576ffb3074869acd884fb48b3f0/packages/services/src/contents/index.ts#L787-L789

At the moment, one option is to right-click on the file and select "Download", which should work (if it does not, it is a bug). That would download to your local filesystem, and then you could upload it to the Jupyter server if it is somewhere else. Not particularly ergonomic, but doable.

I have also been toying with the idea of a button for "Download a repository" in the filebrowser, which downloads the whole zip from GitHub. Do you think that would be a useful thing?

[beenje]

No problem. Thanks for the answer and the link!

If it was in Python, I'd probably try right away. I'm still a newbie in TypeScript/JavaScript and I guess it's not trivial :-)

Regarding the "Download a repository" button, yes, I think that would be nice to have.

As the copy between drives is a jupyterlab issue, feel free to close this issue.

[dearkafka]

Actually  a very needed feature in this extension