diff options
| author | Son Ho | 2021-12-07 17:51:47 +0100 |
|---|---|---|
| committer | Son Ho | 2021-12-07 17:51:47 +0100 |
| commit | 5b04c0d0475fa8368a361575f7f0084de77ab900 (patch) | |
| tree | 435e3a71768e0da7d87ea1949af03d731110a9dc /.gitignore | |
| parent | 119de329f565281f5260b00cbc5fb623f6076ed4 (diff) | |
Update the .gitignore
Diffstat (limited to '.gitignore')
| -rw-r--r-- | .gitignore | 4 |
1 files changed, 3 insertions, 1 deletions
@@ -31,4 +31,6 @@ _opam/ # Misc *~ nohup.out -.ocamlformat
\ No newline at end of file +.ocamlformat +*# +*.lock
\ No newline at end of file |