From 8ed260ed614582e842c0adaf316ec8e938ccf05e Mon Sep 17 00:00:00 2001 From: Jeremie Dimino Date: Wed, 25 Apr 2018 17:46:38 +0100 Subject: [PATCH] jbuild-workspace.dev --> dune-workspace.dev --- Makefile | 2 +- jbuild-workspace.dev => dune-workspace.dev | 0 2 files changed, 1 insertion(+), 1 deletion(-) rename jbuild-workspace.dev => dune-workspace.dev (100%) diff --git a/Makefile b/Makefile index cde32d45d232..ba6526f4e7ad 100644 --- a/Makefile +++ b/Makefile @@ -35,7 +35,7 @@ promote: accept-corrections: promote all-supported-ocaml-versions: - $(BIN) build --dev @install @runtest --workspace jbuild-workspace.dev --root . + $(BIN) build --dev @install @runtest --workspace dune-workspace.dev --root . clean: $(BIN) clean diff --git a/jbuild-workspace.dev b/dune-workspace.dev similarity index 100% rename from jbuild-workspace.dev rename to dune-workspace.dev