diff options
| author | sternenseemann <git@lukasepple.de> | 2020-04-30 20:11:20 +0200 |
|---|---|---|
| committer | sternenseemann <git@lukasepple.de> | 2020-04-30 20:11:20 +0200 |
| commit | f592360503f99dce3966cdc6fdad1d2728fd6fe6 (patch) | |
| tree | 6badaf2e7448da33156b5d873f82db233ce36155 | |
| parent | c8f2f3a0e9b963c2904deac0e2d9624c099a7af9 (diff) | |
Cleanup of old, unused tooling files
| -rw-r--r-- | .gitignore | 2 | ||||
| -rw-r--r-- | .merlin | 4 | ||||
| -rw-r--r-- | .ocp-indent | 1 |
3 files changed, 1 insertions, 6 deletions
diff --git a/.gitignore b/.gitignore index 5a01a1d..84542dd 100644 --- a/.gitignore +++ b/.gitignore @@ -8,4 +8,4 @@ tmp *.byte # nix result -src/.merlin +.merlin diff --git a/.merlin b/.merlin deleted file mode 100644 index 68ac453..0000000 --- a/.merlin +++ /dev/null @@ -1,4 +0,0 @@ -PKG bytes astring angstrom ptime -S src -S test -B _build/** diff --git a/.ocp-indent b/.ocp-indent deleted file mode 100644 index 6c5b8f4..0000000 --- a/.ocp-indent +++ /dev/null @@ -1 +0,0 @@ -strict_with=always,match_clause=4,strict_else=never |