You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Copy file name to clipboardExpand all lines: .gitpod-setup-trac-remote.sh
+4-23Lines changed: 4 additions & 23 deletions
Original file line number
Diff line number
Diff line change
@@ -3,27 +3,8 @@
3
3
# Exit on error
4
4
set -e
5
5
6
-
# Setup trac as remote
7
-
## In order to push to trac, generate a new key with `ssh-keygen -f tempkey` and save the private key to gitpod `gp env PRIVATE_SSH_KEY="$(<tempkey)"` (or by following https://www.gitpod.io/docs/environment-variables#using-the-account-settings)
8
-
## then follow https://doc.sagemath.org/html/en/developer/trac.html#linking-your-public-key-to-your-trac-account to register the public key with trac.
9
-
## Afterwards, create a new gitpod workspace.
10
-
git remote remove trac 2> /dev/null ||true# might still exists from a previous run/prebuild
11
-
if [[ -n"${PRIVATE_SSH_KEY}" ]];then
12
-
# Setup ssh key for authentication with trac
13
-
mkdir -p ~/.ssh
14
-
echo$PRIVATE_SSH_KEY| sed 's/\(-----\(BEGIN\|END\) OPENSSH PRIVATE KEY-----\)/\n\1\n/g'>~/.ssh/id_rsa
0 commit comments