From be5e48b137c1d684bcfdd7acd86ad5fe34c9a04c Mon Sep 17 00:00:00 2001
From: FelixBrendel <felix.brendel@freenet.de>
Date: Wed, 20 May 2020 23:41:38 +0200
Subject: [PATCH] added deinit_printer

---
 print.hpp | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/print.hpp b/print.hpp
index 4220b79..6d293ad 100644
--- a/print.hpp
+++ b/print.hpp
@@ -405,6 +405,11 @@ int print_ptr(FILE* f, void* ptr) {
     return print_to_file(f, "nullptr");
 }
 
+void deinit_printer() {
+    printer_map.dealloc();
+    type_map.dealloc();
+}
+
 void init_printer() {
     printer_map.alloc();
     type_map.alloc();