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.
---
 Makefile.dev | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Makefile.dev')

diff --git a/Makefile.dev b/Makefile.dev
index 54710b6690..9659f602d7 100644
--- a/Makefile.dev
+++ b/Makefile.dev
@@ -17,7 +17,7 @@
 
 .PHONY: devel printers
 
-DEBUGPRINTERS:=dev/top_printers.cmo dev/vm_printers.cmo dev/checker_printers.cmo
+DEBUGPRINTERS:=dev/top_printers.cmo dev/vm_printers.cmo
 
 devel: printers
 printers: $(CORECMA) $(DEBUGPRINTERS)
-- 
cgit v1.2.3