From 0d8292048ed33f4a3736bbd58996e73e64a2efca Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Gr=C3=A9goire=20Henry?= Date: Fri, 22 Sep 2017 17:40:07 +0200 Subject: [PATCH] Ignore local `_opam` switch --- .dockerignore | 2 ++ .gitignore | 2 ++ 2 files changed, 4 insertions(+) diff --git a/.dockerignore b/.dockerignore index d71f9e407..5d0d48199 100644 --- a/.dockerignore +++ b/.dockerignore @@ -47,3 +47,5 @@ test/LOG.* **/*.rej **/*.orig + +_opam \ No newline at end of file diff --git a/.gitignore b/.gitignore index 0a6c74607..4fb464122 100644 --- a/.gitignore +++ b/.gitignore @@ -46,3 +46,5 @@ bisect*.out *.rej *.orig + +/_opam \ No newline at end of file