tree 59e6a563526542e9c9f162d6667f441db1e7c899
parent 802543a5eca6895db068bbd8cbb45bb0577c216e
author Philipp Wagner <phw@lowrisc.org> 1567253464 +0100
committer Philipp Wagner <mail@philipp-wagner.com> 1567260160 +0100

[doc] Remove command to disable push

When using the [hub](https://github.com/github/hub) command line tool it
is not possible to set non-URLs as remote:

```
$ git remote set-url --push upstream disabled
Error: repository disabled/opentitan doesn't exist
```

Removing this instruction from the user guide to prevent confusion for
users who have this tool installed.