First time here? Check out the FAQ!

Ask Your Question
0

How to push from the cloud to github?

asked 9 years ago

Erel Segal-Halevi gravatar image

I opened a new project in the SageMath cloud, and imported a GitHub project using the "Download from web" button.

I made some changes in the files on the cloud.

In the "Terminal command..." window in the top-right, I did "git add -A", then "git commit -m ''", then "git push".

The last command generated the following error:

fatal: could not read Username for 'https://github.com': No such device or address

I found some solutions to this error, but I don't know which, if any, are appropriate to the SageMath cloud.

Is it possible to push changes made on the cloud back to GitHub?

Preview: (hide)

Comments

A SageMathCloud project is just a standard Linux account, running on Ubuntu 15.04 right now.

William Stein gravatar imageWilliam Stein ( 9 years ago )

2 Answers

Sort by » oldest newest most voted
1

answered 9 years ago

ianhi gravatar image

Hi, I am experiencing the same error as you when I use the terminal window in the top right of the file browser. Based on this thread I think the issue has something to do with whether you are connecting to github via ssh or https.

WORKAROUND: The workaround is very simple:
1. Make a .term file instead of using the terminal box
2. use the .term file to run your git command

This worked for me, I hope it solves your problem

Preview: (hide)
link

Comments

Where do you create the term file? And what exactly is in that file?

Erel Segal-Halevi gravatar imageErel Segal-Halevi ( 9 years ago )

You can create a .term file from the interface brought up by the "+New" button on the top left, then choose the ">_terminal" button. This gives you a full interactive linux command line.

ianhi gravatar imageianhi ( 9 years ago )

This worked. Thanks!

Erel Segal-Halevi gravatar imageErel Segal-Halevi ( 9 years ago )
0

answered 9 years ago

haraldschilly gravatar image

what does git remote -v say? are you using the https:// instead of the git:// URL?

Preview: (hide)
link

Comments

OK, I changed to using the git URL. Now, "git remote -v" shows:

origin  git@github.com:erelsgl/envy-free.git (fetch)
origin  git@github.com:erelsgl/envy-free.git (push)

and "git push" shows:

Host key verification failed.
fatal: Could not read from remote repository.

Please make sure you have the correct access rights
and the repository exists.
Erel Segal-Halevi gravatar imageErel Segal-Halevi ( 9 years ago )

I thought it is related to SSH keys, so I tried to generate a key by:

ssh-keygen -t rsa -b 4096 -C "erelsgl@gmail.com"

But, I got the following error:

Timed out after 10 seconds.
Erel Segal-Halevi gravatar imageErel Segal-Halevi ( 9 years ago )

Your Answer

Please start posting anonymously - your entry will be published after you log in or create a new account.

Add Answer

Question Tools

1 follower

Stats

Asked: 9 years ago

Seen: 1,492 times

Last updated: Nov 04 '15