summaryrefslogtreecommitdiff
path: root/.gitignore
diff options
context:
space:
mode:
authorSon Ho2022-01-26 22:48:50 +0100
committerSon Ho2022-01-26 22:48:50 +0100
commita2a40e7f39990f9d777e91d4b2f3957f5e70d685 (patch)
tree266311f6a96d8fd91a504b06599f5f30cc0c065a /.gitignore
parentcd9ed7e816f76119a321a8e2185e5244ad1d111a (diff)
Update the .gitignore
Diffstat (limited to '.gitignore')
-rw-r--r--.gitignore3
1 files changed, 2 insertions, 1 deletions
diff --git a/.gitignore b/.gitignore
index 592ae076..7b7e4e7f 100644
--- a/.gitignore
+++ b/.gitignore
@@ -37,4 +37,5 @@ nohup.out
.ocamlformat
*#
*.lock
-*.txt \ No newline at end of file
+*.txt
+*/.#* \ No newline at end of file