diff options
| author | Pierre-Marie Pédrot | 2020-07-10 23:29:05 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-07-17 15:16:12 +0200 |
| commit | f41fccaaf30ea4f76edb8204fa5f4022467b6e0c (patch) | |
| tree | 630d6102b775dbde3e5d353626b5b988264ed9cf | |
| parent | de89e569c1816e9b2ea5b0ad30b03d18bd71fd64 (diff) | |
Remove automatic formatting of ComHints.
This is about the third time I try to kill this file but for some reason
it is still here.
| -rw-r--r-- | vernac/.ocamlformat-enable | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/vernac/.ocamlformat-enable b/vernac/.ocamlformat-enable deleted file mode 100644 index ffaa7e70f4..0000000000 --- a/vernac/.ocamlformat-enable +++ /dev/null @@ -1 +0,0 @@ -comHints.ml |