Skip to content

Commit

Permalink
jbuild-workspace.dev --> dune-workspace.dev
Browse files Browse the repository at this point in the history
  • Loading branch information
Jeremie Dimino committed Apr 25, 2018
1 parent a031159 commit 0210777
Show file tree
Hide file tree
Showing 2 changed files with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
File renamed without changes.

0 comments on commit 0210777

Please sign in to comment.