Skip to content

Commit 273a82b

Browse files
committed
Minor edits on workspace.rst
1 parent a388bba commit 273a82b

File tree

1 file changed

+9
-9
lines changed

1 file changed

+9
-9
lines changed

src/doc/en/developer/workspace.rst

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -8,10 +8,10 @@ Setting up your workspace
88

99
.. _section-ide:
1010

11-
Configuring text editors and IDEs for use with Sage
12-
===================================================
11+
Text editors and IDEs for use with Sage
12+
=======================================
1313

14-
In Meta-Issue :issue:`30500` we are collecting instructions how to configure
14+
In meta :issue:`30500` we are collecting instructions how to configure
1515
various text editors and IDEs for use with Sage.
1616

1717

@@ -34,12 +34,12 @@ You can now run and edit Sage's code. Contributing your changes follows the norm
3434
:ref:`Git workflow <chapter-git-basic>`.
3535
For this to work, you first have to authorize Gitpod with GitHub:
3636

37-
1. In the running Gitpod workspace, generate a new SSH key pair by ``ssh-keygen -f tempkey``.
38-
2. Save the private key as a secure environment variable in Gitpod using
39-
``gp env PRIVATE_SSH_KEY="$(<tempkey)"``,
40-
or by using the `Gitpod UI <https://www.gitpod.io/docs/environment-variables#using-the-account-settings>`_.
41-
3. Register the public key with GitHub following the instructions in :ref:`section-github-ssh-key`.
42-
4. Close this Gitpod workspace.
37+
1. In the running Gitpod workspace, generate a new SSH key pair by ``ssh-keygen -f tempkey``.
38+
2. Save the private key as a secure environment variable in Gitpod using ``gp
39+
env PRIVATE_SSH_KEY="$(<tempkey)"``, or by using the `Gitpod UI
40+
<https://www.gitpod.io/docs/environment-variables#using-the-account-settings>`_.
41+
3. Register the public key with GitHub following the instructions in :ref:`section-github-ssh-key`.
42+
4. Close this Gitpod workspace.
4343

4444
After following this procedure, every new Gitpod workspace will have a
4545
working ``origin`` remote to which you can push your changes.

0 commit comments

Comments
 (0)