diff options
| author | Emilio Jesus Gallego Arias | 2018-11-09 19:15:54 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-11-09 19:15:54 +0100 |
| commit | ce8e37b97ce9db6f39368c50fb0ee4a7839ce754 (patch) | |
| tree | a6678760bcd97cf004ba1f065352c8cad666bec3 /dev/doc | |
| parent | 7e3c54c09bdd748e2e2a60a94891b65481776041 (diff) | |
| parent | a7522a0ea76a6efaed9342d08a95363b56d88d32 (diff) | |
Merge PR #8949: Remove checker printers
Diffstat (limited to 'dev/doc')
| -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 0aeb30c4e8..c5ea88aaf6 100644 --- a/dev/doc/build-system.dune.md +++ b/dev/doc/build-system.dune.md @@ -81,7 +81,7 @@ or ``` dune exec dev/dune-dbg checker -(ocd) source checker_dune_db +(ocd) source dune_db ``` for the checker. Unfortunately, dependency handling here is not fully |