Provide a dedicated interface for destroying open menus.

Add ro_gui_menu_destroy(), so that this specific task does not share the same code as the more general task of tidying up after menus have been closed by other means.
The original ro_gui_menu_closed() now simply cleans up from a known (or assumed) closure, without forcing a closure itself.

1 files changed, 1 insertions, 1 deletions

diff --git a/riscos/print.c b/riscos/print.c
index 09d4aaefb..c539f011c 100644
--- a/riscos/print.c
+++ b/riscos/print.c
@@ -525,7 +525,7 @@ void ro_print_cleanup(void)
 	print_text_black = false;
 	print_prev_message = 0;
 	print_max_sheets = -1;
-	ro_gui_menu_closed();
+	ro_gui_menu_destroy();
 	ro_gui_dialog_close(dialog_print);
 }