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;