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

agda.section.md: Fix header and enumeration #98084

Merged
merged 2 commits into from
Oct 11, 2020
Merged

Conversation

turion
Copy link
Contributor

@turion turion commented Sep 16, 2020

CC @alexarice

/marvin opt-in
/status needs_reviewer

@turion
Copy link
Contributor Author

turion commented Sep 16, 2020

The enumeration isn't fixed yet. Let me amend.

@ofborg ofborg bot added the 8.has: documentation This PR adds or changes documentation label Sep 16, 2020
@turion
Copy link
Contributor Author

turion commented Sep 16, 2020

/marvin opt-in
/status needs_reviewer

@marvin-mk2 marvin-mk2 bot added the marvin This PR was reviewed by Marvin, a discontinued bot: https://github.com/timokau/marvin-mk2 label Sep 16, 2020
@marvin-mk2
Copy link

marvin-mk2 bot commented Sep 16, 2020

Hi! I'm an experimental bot. My goal is to guide this PR through its stages, hopefully ending with a merge. You can read up on the usage here.

@marvin-mk2 marvin-mk2 bot added the needs_reviewer (old Marvin label, do not use) label Sep 16, 2020
@ofborg ofborg bot added 10.rebuild-darwin: 0 This PR does not cause any packages to rebuild on Darwin 10.rebuild-linux: 0 This PR does not cause any packages to rebuild on Linux labels Sep 16, 2020
Copy link
Contributor

@alexarice alexarice left a comment

Choose a reason for hiding this comment

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

Thanks for catching these, This probably needs to be backported once finished

doc/languages-frameworks/agda.section.md Outdated Show resolved Hide resolved
doc/languages-frameworks/agda.section.md Outdated Show resolved Hide resolved
@marvin-mk2 marvin-mk2 bot added awaiting_reviewer (old Marvin label, do not use) and removed needs_reviewer (old Marvin label, do not use) labels Sep 16, 2020
@turion turion mentioned this pull request Sep 16, 2020
10 tasks
@ofborg ofborg bot added the 6.topic: nixos Issues or PRs affecting NixOS modules, or package usability issues specific to NixOS label Sep 16, 2020
Copy link
Contributor

@alexarice alexarice left a comment

Choose a reason for hiding this comment

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

Looks good, could you rebase down to 1 or 2 commits?

@marvin-mk2 marvin-mk2 bot added needs_reviewer (old Marvin label, do not use) and removed awaiting_reviewer (old Marvin label, do not use) labels Sep 21, 2020
@alexarice alexarice mentioned this pull request Sep 23, 2020
10 tasks
@nixos-discourse
Copy link

This pull request has been mentioned on NixOS Discourse. There might be relevant details there:

https://discourse.nixos.org/t/prs-already-reviewed/2617/244

@marvin-mk2 marvin-mk2 bot added awaiting_reviewer (old Marvin label, do not use) and removed needs_reviewer (old Marvin label, do not use) labels Oct 11, 2020
@kevincox kevincox merged commit 8b33d57 into NixOS:master Oct 11, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
6.topic: nixos Issues or PRs affecting NixOS modules, or package usability issues specific to NixOS 8.has: documentation This PR adds or changes documentation 10.rebuild-darwin: 0 This PR does not cause any packages to rebuild on Darwin 10.rebuild-linux: 0 This PR does not cause any packages to rebuild on Linux awaiting_reviewer (old Marvin label, do not use) marvin This PR was reviewed by Marvin, a discontinued bot: https://github.com/timokau/marvin-mk2
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants