diff options
| author | Enrico Tassi | 2019-03-08 16:30:30 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2019-03-31 14:33:40 +0200 |
| commit | ed996432fd079583afbb1797c92ad23f654b94eb (patch) | |
| tree | 4f677d1a1f2113208e5129f9011dcfd09c312508 | |
| parent | 44e5afe99d8b40c3ed0d546f56a446427c7c4da4 (diff) | |
[dune] typo
| -rw-r--r-- | dev/doc/build-system.dune.md | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md index b1bfac8cc9..49251d61a1 100644 --- a/dev/doc/build-system.dune.md +++ b/dev/doc/build-system.dune.md @@ -22,7 +22,7 @@ If you want to build the standard libraries and plugins you should call `make -f Makefile.dune voboot`. It is usually enough to do that once per-session. -More helper targets are availabe in `Makefile.dune`, `make -f +More helper targets are available in `Makefile.dune`, `make -f Makefile.dune` will display some help. Dune places build artifacts in a separate directory `_build`; it will |