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

chore: make missing records fields an error for cryptol-remote-api #1088

Merged
merged 1 commit into from
Feb 24, 2021

Conversation

pnwamk
Copy link
Contributor

@pnwamk pnwamk commented Feb 23, 2021

No description provided.

@pnwamk pnwamk force-pushed the no-missing-record-fields branch from 970f03a to 40ba4a4 Compare February 23, 2021 23:46
@pnwamk pnwamk requested a review from robdockins February 24, 2021 00:18
@pnwamk
Copy link
Contributor Author

pnwamk commented Feb 24, 2021

Fix remote server w.r.t. changes in b3d142a and turn missing record fields into an error to avoid further changes sneaking by without notice.

@pnwamk pnwamk removed the request for review from robdockins February 24, 2021 21:14
@pnwamk pnwamk force-pushed the no-missing-record-fields branch from 40ba4a4 to 9be8bde Compare February 24, 2021 21:31
@pnwamk pnwamk merged commit 665b1c7 into master Feb 24, 2021
@pnwamk pnwamk deleted the no-missing-record-fields branch February 24, 2021 22:14
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.

1 participant