diff options
author | Son Ho | 2022-01-26 22:48:50 +0100 |
---|---|---|
committer | Son Ho | 2022-01-26 22:48:50 +0100 |
commit | a2a40e7f39990f9d777e91d4b2f3957f5e70d685 (patch) | |
tree | 266311f6a96d8fd91a504b06599f5f30cc0c065a | |
parent | cd9ed7e816f76119a321a8e2185e5244ad1d111a (diff) |
Update the .gitignore
-rw-r--r-- | .gitignore | 3 |
1 files changed, 2 insertions, 1 deletions
@@ -37,4 +37,5 @@ nohup.out .ocamlformat *# *.lock -*.txt
\ No newline at end of file +*.txt +*/.#*
\ No newline at end of file |