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
Similarly to git remote set-url --add this option would be useful to simplify things like opam remote add <name> <url> || opam remote set-url <name> <url> in scripts or other "steps to follow" used to make sure the recipient has the correct remote at the correct url.
As a side-note, opam remote add <name> <url> currently does not return an error when url is the current url of the repository name but does return an error when it's not, whereas git remote will raise an error in both cases.
The text was updated successfully, but these errors were encountered:
Similarly to
git remote set-url --add
this option would be useful to simplify things likeopam remote add <name> <url> || opam remote set-url <name> <url>
in scripts or other "steps to follow" used to make sure the recipient has the correct remote at the correct url.As a side-note,
opam remote add <name> <url>
currently does not return an error whenurl
is the current url of the repositoryname
but does return an error when it's not, whereasgit remote
will raise an error in both cases.The text was updated successfully, but these errors were encountered: