From a7522a0ea76a6efaed9342d08a95363b56d88d32 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 8 Nov 2018 15:01:24 +0100
Subject: Remove checker printers

Now that the checker is using the regular kernel files it can also use
the normal printers.
---
 dev/doc/build-system.dune.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev/doc')

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
-- 
cgit v1.2.3