Skip to content
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

Add hostname option #98

Merged
merged 1 commit into from
Oct 14, 2020
Merged

Add hostname option #98

merged 1 commit into from
Oct 14, 2020

Conversation

hazelweakly
Copy link
Contributor

Set the PR into this branch because that's what saw-script is currently pulling in as a submodule.

Copy link
Contributor

@david-christiansen david-christiansen left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This looks good to me.

@atomb, do you think this should go onto the designated branch, or into master? I don't have a lot of insight into how you're working through the server code transition, or what would be most convenient there.

argo/src/Argo/DefaultMain.hs Outdated Show resolved Hide resolved
@david-christiansen
Copy link
Contributor

Now that #93 and #92 are merged, I do think this should target master instead.

@hazelweakly hazelweakly changed the base branch from at-move-cryptol-remote-api to master October 13, 2020 22:10
@hazelweakly
Copy link
Contributor Author

I updated it to target master instead.

@david-christiansen david-christiansen merged commit 5f5ee6f into master Oct 14, 2020
@david-christiansen
Copy link
Contributor

Thank you!

@hazelweakly hazelweakly deleted the add-hostname branch October 14, 2020 21:57
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants