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)