Use the JupyterHub Git extension#
This page is under construction.
We’re still working on this page.
Please check back in a few days; we’re sorry for the inconvenience.
The SigTech team
Monday, 09 December 2024 (11:48)
When you are added to a workspace as a member, SigTech sets up a user branch of the workspace GitHub repo for you.
The first time you start a research environment with the workspace, SigTech clones (makes a copy of) the workspace for you. This means that each workspace member has their own copy of the files in the workspace.
Your copy of the workspace (what you see when you start a research environment) is referred to as your local repo.
Your named user branch within your local repo is referred to as your local user branch.
Your named user branch on GitHub is referred to as your remote user branch.
When you use the SigTech platform to create, delete, and modify the files in a workspace, you commit to your local user branch.
When you use the SigTech platform to publish your changes, you push to your remote user branch.
To merge your changes so that other workspace members can see them, you need to make a pull request from your remote user branch to the default branch of the remote repo.
Create a pull request in GitHub#
This section only applies to workspaces in protected main mode.
If your workspace is in simple mode, you can push directly to the default branch of the workspace GitHub repo from the SigTech platform.
See also
[Use the JupyterHub Git extension][8]
In your browser, go to the GitHub repo for your workspace.
Note that:
All of your company’s workspace repos are in your GitHub organization account.
A workspace’s GitHub repo name contains the organization name, the username of the person who created it, and the workspace name.
To find a workspace’s GitHub repo name, in go to the Workspaces tab in the SigTech platform. You’ll see a list of workspaces and their corresponding GitHub repos.
Here’s an example GitHub URL for a workspace named “test-workspace”, created by Jennie from Some Org (Jennie’s GitHub username is
jennie-ling
):https://github.com/SomeOrg/someorg-jennie-ling-test-workspace
In GitHub, go to Pull requests and select New pull request.
For the base branch, select the main branch.
For the branch to compare, select
users/your-username
.Add a title and, optionally, a description for the pull request. Then, select Create pull request.
Depending on your organization, your pull request might need approval before it can be merged.
When your pull request has been merged, you can continue working on your branch in the SigTech research environment.
If you’re collaborating with colleagues, it’s probably a good idea to regularly sync changes from GitHub to your workspace.