-
Notifications
You must be signed in to change notification settings - Fork 38
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
dune-release publish distrib use the wrong uri #172
Comments
For more context: with my configuration, the correct uri would be I can think of 2 fixes:
This problem can also happen to users that don't use ssh. In that case, the user may (or may not if configured correctly) interact with |
A quick fix for that would be to offer you to skip that step so that you can push the tag yourself and leave the rest to A next step could be to allow local release configurations so that you can tell |
Looks good to me :) |
For me dune-release wants to push the tags to
This fails with But my remote is |
Hmm that one's weird. Thanks for reporting it, we'll look into it! |
I think this issue is obsolete. Dune-release still has issues with my URLs, though: #479 |
dune-release publish distrib
tries to push the git tag to a made up uri:That uri won't match any key in my config and the push will fail.
Answering
n
will abort the whole procedure, so I can't push manually and skip this step.The text was updated successfully, but these errors were encountered: