Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

feat(tactic/doc_blame): Use is_auto_generated #1395

Merged
merged 2 commits into from
Sep 4, 2019
Merged

feat(tactic/doc_blame): Use is_auto_generated #1395

merged 2 commits into from
Sep 4, 2019

Conversation

PatrickMassot
Copy link
Member

@PatrickMassot PatrickMassot requested a review from a team as a code owner September 3, 2019 20:43
@fpvandoorn
Copy link
Member

lgtm

@jcommelin
Copy link
Member

Even though I'm not one of these brilliant tactic writers myself, I feel confident merging this one (-;

@jcommelin jcommelin added the ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) label Sep 4, 2019
@mergify mergify bot merged commit b079298 into master Sep 4, 2019
@mergify mergify bot deleted the doc-blame-fix branch September 4, 2019 06:34
anrddh pushed a commit to anrddh/mathlib that referenced this pull request May 15, 2020
@PatrickMassot @anrddh
feat(tactic/doc_blame): Use is_auto_generated (leanprover-community#1395
28bb428 
)
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Reviewers

@jcommelin jcommelin jcommelin approved these changes

Assignees
No one assigned
Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@PatrickMassot @fpvandoorn @jcommelin