diff options
| author | Cyril Cohen | 2020-03-12 11:52:22 +0100 |
|---|---|---|
| committer | GitHub | 2020-03-12 11:52:22 +0100 |
| commit | bf4ddf1894c6ac63dffae2bdad8f8c5300ba0954 (patch) | |
| tree | f54adba22ff99ab008ad18ed089ae6946670260d /etc/utils | |
| parent | 7d04173b52cf02717b8f8e8c13bb7c3521de7e89 (diff) | |
| parent | 3ae871fff2165c27b8bb389f1829766a4d6f00d9 (diff) | |
Merge pull request #455 from erikmd/bump-opam
[ci] Simplify {Dockerfile,Dockerfile.make} & Restore the "opam clean -c" option
Diffstat (limited to 'etc/utils')
0 files changed, 0 insertions, 0 deletions