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.

Sign up for GitHub

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

Jump to bottom

Fix gitattributes for Makefile.dune #9653

Merged
merged 1 commit into from Feb 26, 2019
Merged

Fix gitattributes for Makefile.dune #9653

merged 1 commit into from Feb 26, 2019

Conversation

SkySkimmer
Copy link
Contributor

Since it matches .dune and Makefile the later needs to come second
in the gitattributes file.

@SkySkimmer
Fix gitattributes for Makefile.dune
f0896b9 
Since it matches *.dune and Makefile* the later needs to come second
in the gitattributes file.
@ejgallego ejgallego self-assigned this Feb 26, 2019
@ejgallego ejgallego added the kind: infrastructure CI, build tools, development tools. label Feb 26, 2019
@ejgallego ejgallego added this to the 8.10+beta1 milestone Feb 26, 2019
@ejgallego
Copy link
Member

Thanks I was hit by this.

@ejgallego ejgallego merged commit f0896b9 into coq:master Feb 26, 2019
ejgallego added a commit that referenced this pull request Feb 26, 2019
@ejgallego
Merge PR #9653: Fix gitattributes for Makefile.dune
45ad16b
@SkySkimmer SkySkimmer deleted the fix-gitattr-dune branch February 26, 2019 13:01
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees

@ejgallego ejgallego

Labels
kind: infrastructure CI, build tools, development tools.
Projects
None yet
Milestone
8.10+beta1
Development

Successfully merging this pull request may close these issues.

None yet
2 participants
@SkySkimmer @ejgallego