Skip to content

Commit 68f4c9a

Browse files
authored
Update Coq.gitignore
Coq now uses .mlg rather than .ml4 (since rocq-prover/rocq#8763), so we have to ignore its generated dependency files. The `native_compute_profile_*.data` files are generated by `Set NativeCompute Profiling` (see rocq-prover/rocq#950). Finally `.coq-native` is a directory that may be generated in any subdirectory, not only at top level, so we should not use absolute paths for it.
1 parent 218a941 commit 68f4c9a

File tree

1 file changed

+3
-1
lines changed

1 file changed

+3
-1
lines changed

Coq.gitignore

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,7 @@
1010
*.glob
1111
*.ml.d
1212
*.ml4.d
13+
*.mlg.d
1314
*.mli.d
1415
*.mllib.d
1516
*.mlpack.d
@@ -20,7 +21,7 @@
2021
*.vo
2122
*.vok
2223
*.vos
23-
.coq-native/
24+
.coq-native
2425
.csdp.cache
2526
.lia.cache
2627
.nia.cache
@@ -31,6 +32,7 @@ lia.cache
3132
nia.cache
3233
nlia.cache
3334
nra.cache
35+
native_compute_profile_*.data
3436

3537
# generated timing files
3638
*.timing.diff

0 commit comments

Comments
 (0)