restart your binder - say you visited Binder to start the binder, but now changes have been made on GitHub: visit Binder again. You’ll get a new binder session with the changes.
Open a terminal in your running Binder session and use git to fetch and merge the latest changes from GitHub. Should be something like git fetch && git merge origin/master.
Which of the two you want to do depends a bit on how much you’ve edited in your Binder session and how much has changed.
Thanks. The git update in the terminal works - as long as I stay in this browser session. i.e. I now have a session where I see my files having been updated 2 minutes ago.
However, if I copy&paste the binder link into a 2nd browser (-> a person I’d like to share this with), it starts a new binder where the files are again > 1hour old, so no update there.
(sorry, I really don’t fully grasp what’s going on in the background there…)
That shouldn’t happen. They should see the latest&greatest version. Do you have a link to the repository you are using? Without it it is very hard to say anything specific/helpful.
This is behaving as expected- the binder link button gives you a link to the github commit used to launch your binder, the idea being that it’s fully reproducible. If you launch a new server using your original GitHub repo it should be up to date. If it isn’t then please share your repo as @betatim suggests.
About an hour later, the Firefox session in which I pulled the updates from github times out, i.e. I get a 404 on a page reload and re-opening it from the original binder link, I’m back to where I started, last changes 18 hour ago.
Did you get the link to the repository from the “Copy Binder link” in the top right corner of the UI?
yes I did
so now I tried the head link which now lists files being modified 3h ago but the last commit on the repo was yesterday? does it pick up any changes which were made in the binder meanwhile?
Also, and that smells like a bug: after having loaded with the head link, I still get a non-head link when I click the “Copy Binder Link” button, this time Binder
Meanwhile, I pushed another change to the github repo, restarted the binder with the head link, this time it created a new container (although there was no change to the environment/module requirements). “Copy Binder Link” button still creates a non-head link, though.
I think this is one of those cases where others would argue what one person views as a bug is a ‘feature’ to others. For example, if you are en educator and you want to share the exact version you are running with trainees, you can grab the link there and share it in the moment instead of taking the time to build it yourself. The mybinder.org main page will always generate the main link you’d want to use in either .md or .rst or even plain URL form. It is a good practice to place that bit of code that on your README page when you are developing. For example, note the launch binder button on the main page of the spaCy course repo. Then you are anyone you want to share it with has something to click on or you can get the URL via right-click Copy Link from there to collect the URL to email people.
Before the addition of the copy Binder link button in the running sessions, a lot of people were sharing the ephemeral running link which would expire 10 minutes later most of the time. So at least you and your colleagues got a working session even if you didn’t pick up on the git tag at the end linking to specific version.
You can even make custom binder launch badges here. For example for a repo for special genomics software where some folks would be more familiar with the software than Jupyter, I made a badge that says launch Circos on Jupyter. There’s even a way to make badges for pull requests using Github actions.
When you start a binder then the last part of the URL specifies which revision to take from the GitHub repository.
90% of mybinder.org links end in /master or /main, which means they get built from the last commit on the master or main branch at the time you click the link. Some links end in a particular commit SHA1. These always build a container for that particular commit.
@fomightez described why the “copy binder link” button behaves how it does. Based on (lack of) forum posts about its behaviour it seems it mostly does what people expect, but sometimes it catches someone out. A nice solution to cover both cases without totally confusing a new user who doesn’t know what they want/need/only half listened to their instructor would be great to have. However it is a tricky problem to solve :-/
I think this is because the “modified date” of a file in a docker image is set to the time it is created. So when you do git checkout the date is set to the time you run that command, not when the commit was originally made.
