diff options
| author | Son Ho | 2021-11-19 18:26:00 +0100 |
|---|---|---|
| committer | Son Ho | 2021-11-19 18:26:00 +0100 |
| commit | 4a28b75fe834878b1c93d1fe6fe8a02576957f75 (patch) | |
| tree | 8c968f4fffccabdad88ef52ac6c7617b10c7ba3b /.gitignore | |
| parent | ef830bd7bedcad8b465aa4ac92cff30649426ea4 (diff) | |
Start working on pretty-printing
Diffstat (limited to '.gitignore')
| -rw-r--r-- | .gitignore | 3 |
1 files changed, 2 insertions, 1 deletions
@@ -30,4 +30,5 @@ _opam/ # Misc *~ -nohup.out
\ No newline at end of file +nohup.out +.ocamlformat
\ No newline at end of file |