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

Open
wants to merge 2 commits into
base: master
from
Open

Conversation

@turion
Copy link
Contributor

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.

@turion turion force-pushed the turion:patch-5 branch from 407402c to 499b0c2 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 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.

Copy link
Contributor

alexarice left a comment

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
@turion turion mentioned this pull request Sep 16, 2020
3 of 10 tasks complete
@turion turion force-pushed the turion:patch-5 branch from ca7928d to 9a360fe Sep 16, 2020
@ofborg ofborg bot added the 6.topic: nixos label Sep 16, 2020
Copy link
Contributor

alexarice left a comment

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

@turion turion force-pushed the turion:patch-5 branch from f62b4bb to 4336f9f Sep 18, 2020
@alexarice alexarice mentioned this pull request Sep 23, 2020
1 of 5 tasks complete
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Linked issues

Successfully merging this pull request may close these issues.

None yet

2 participants
You can’t perform that action at this time.