diff --git a/repos/ports/src/app/seoul/user_env.cc b/repos/ports/src/app/seoul/user_env.cc
index 9954ae5f55..4c76bb86da 100644
--- a/repos/ports/src/app/seoul/user_env.cc
+++ b/repos/ports/src/app/seoul/user_env.cc
@@ -135,12 +135,26 @@ void operator delete[](void *ptr)
 		Genode::warning("delete[] not implemented ", ptr);
 }
 
+
+void operator delete[](void *ptr, long unsigned int)
+{
+	if (verbose_memory_leak)
+		Genode::warning("delete[] not implemented ", ptr);
+}
+
+
 void operator delete (void * ptr)
 {
 	heap_free(ptr);
 }
 
 
+void operator delete(void *ptr, long unsigned int)
+{
+	heap_free(ptr);
+}
+
+
 void do_exit(char const *msg)
 {
 	Genode::log("*** ", msg);