-
Notifications
You must be signed in to change notification settings - Fork 1
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
Fixup .gitignore #67
Fixup .gitignore #67
Conversation
e76a2ae
to
9597d49
Compare
CI failure fixed in #68 |
9597d49
to
ea8ed6c
Compare
CI failure over! |
ea8ed6c
to
b432d52
Compare
don't merge till #67 lands (or we have to mess with CI rebase again) |
b432d52
to
ff5b6a3
Compare
.gitignore
Outdated
/result* | ||
/target/** |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
We can also remove these two rules, these directories are covered by the two rules above.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yup. That's what I get for having autogenerated .gitignore
From man gitignore: A leading "**" followed by a slash means match in all directories. For example, "**/foo" matches file or directory "foo" anywhere, the same as pattern "foo". In other words, we don't need "/target/**" in the .gitignore if we already have "**/target/**". Same applies to "/result*". Let's remove the redundant rules. Also sort the file alphabetically (as per Vim's ":%s"). Signed-off-by: Quentin Monnet <[email protected]>
I pushed a commit on top of your branch. |
We're good now that we no longer require the base branch to be up-to-date. |
No description provided.