From f3d5cf3e57bec72bf153c1f6efab91525e3e499a Mon Sep 17 00:00:00 2001 From: David Allsopp Date: Sat, 30 Jul 2022 13:13:40 +0200 Subject: [PATCH] Tweak ignored dirs at the root --- .gitignore | 2 +- dune | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/.gitignore b/.gitignore index 1cf08babd59..f6b6ed79d51 100644 --- a/.gitignore +++ b/.gitignore @@ -3,7 +3,7 @@ _obuild/ _opam/ _olint/ .vscode/ -bootstrap/ +/bootstrap*/ tests/tmp/ tests/.merlin tests/reftests/.merlin diff --git a/dune b/dune index ae32277916f..949ffb03df0 100644 --- a/dune +++ b/dune @@ -1 +1 @@ -(dirs :standard \ bootstrap release) +(dirs :standard \ bootstrap* release)