mirror of
https://github.com/github/gitignore.git
synced 2026-08-30 11:47:22 +02:00
Compare commits
15 Commits
4cd1184fd9
...
fd75254a46
| Author | SHA1 | Date | |
|---|---|---|---|
|
|
fd75254a46 | ||
|
|
e9c620b9f6 | ||
|
|
5853962226 | ||
|
|
c5bf3caf29 | ||
|
|
7514684825 | ||
|
|
ad49657df2 | ||
|
|
9ffced6030 | ||
|
|
49990d1d63 | ||
|
|
3d21cef359 | ||
|
|
de90107f1a | ||
|
|
84c6914a9b | ||
|
|
5f760225cf | ||
|
|
b9ad512a45 | ||
|
|
9aa86b4610 | ||
|
|
66b704afbe |
2
Lean.gitignore
Normal file
2
Lean.gitignore
Normal file
@ -0,0 +1,2 @@
|
||||
# cache and other artifacts produced by Lean's Lake build tool
|
||||
.lake/
|
||||
@ -7,7 +7,7 @@ release.properties
|
||||
dependency-reduced-pom.xml
|
||||
buildNumber.properties
|
||||
.mvn/timing.properties
|
||||
# https://maven.apache.org/wrapper/#usage-without-binary-jar
|
||||
# https://maven.apache.org/tools/wrapper/#Usage_with_or_without_Binary_JAR
|
||||
.mvn/wrapper/maven-wrapper.jar
|
||||
|
||||
# Eclipse m2e generated files
|
||||
|
||||
@ -4,3 +4,6 @@ result-*
|
||||
|
||||
# Ignore automatically generated direnv output
|
||||
.direnv
|
||||
|
||||
# Ignore NixOS interactive test driver history
|
||||
**/.nixos-test-history
|
||||
|
||||
@ -24,11 +24,9 @@ We support a collection of templates, organized in this way:
|
||||
with popular programming languages and technologies. These define a meaningful
|
||||
set of rules to help get started, and ensure you are not committing
|
||||
unimportant files into your repository.
|
||||
- [`Global`](./Global) contains templates for various editors, tools and
|
||||
operating systems that can be used in different situations. It is recommended
|
||||
that you either [add these to your global template](https://docs.github.com/en/get-started/getting-started-with-git/ignoring-files#configuring-ignored-files-for-all-repositories-on-your-computer)
|
||||
or merge these rules into your project-specific templates if you want to use
|
||||
them permanently.
|
||||
- [`Global`](./Global) contains templates for various editors, tools, and
|
||||
operating systems that can be used in different situations. We recommend
|
||||
adding these to your [global template](https://docs.github.com/en/get-started/getting-started-with-git/ignoring-files#configuring-ignored-files-for-all-repositories-on-your-computer) or merging these rules into your project-specific templates if you want to use them permanently.
|
||||
- [`community`](./community) contains specialized templates for other popular
|
||||
languages, tools and project, which don't currently belong in the mainstream
|
||||
templates. These should be added to your project-specific templates when you
|
||||
|
||||
@ -75,6 +75,11 @@ acs-*.bib
|
||||
# comment
|
||||
*.cut
|
||||
|
||||
# context
|
||||
*.tuc
|
||||
*.tui
|
||||
*.tuo
|
||||
|
||||
# cprotect
|
||||
*.cpt
|
||||
|
||||
|
||||
Loading…
Reference in New Issue
Block a user