diff options
| author | Gaëtan Gilbert | 2018-11-08 15:01:24 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-11-08 15:01:24 +0100 |
| commit | a7522a0ea76a6efaed9342d08a95363b56d88d32 (patch) | |
| tree | 9ab8bd176949a072e0edb1f79502142cedcdb0b2 /Makefile.dev | |
| parent | 108c15b51a7d5f647c8681fe7a37c86f0c5a8b9c (diff) | |
Remove checker printers
Now that the checker is using the regular kernel files it can also use
the normal printers.
Diffstat (limited to 'Makefile.dev')
| -rw-r--r-- | Makefile.dev | 2 |
1 files changed, 1 insertions, 1 deletions
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) |