From c33928f202fb8fe9e1e8978764949f2ad47e1be7 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 6 Jan 2015 10:22:23 -0800
Subject: [PATCH] fix(library/pp_options): memory leak

---
 src/library/pp_options.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/library/pp_options.cpp b/src/library/pp_options.cpp
index 399b680cc..c876eedba 100644
--- a/src/library/pp_options.cpp
+++ b/src/library/pp_options.cpp
@@ -131,6 +131,7 @@ void initialize_pp_options() {
 }
 
 void finalize_pp_options() {
+    delete g_pp_numerals;
     delete g_pp_max_depth;
     delete g_pp_max_steps;
     delete g_pp_notation;