diff --git a/repos/base-hw/src/core/kernel/cpu.h b/repos/base-hw/src/core/kernel/cpu.h
index 810ed7bc1..4c298140d 100644
--- a/repos/base-hw/src/core/kernel/cpu.h
+++ b/repos/base-hw/src/core/kernel/cpu.h
@@ -69,6 +69,7 @@ namespace Kernel
  *   publicly provide via a 'typedef Genode::Cpu::Arch_regs Arch_regs'.
  *   Then, the 'Genode::Cpu' could be inherited privately.
  */
+#pragma GCC diagnostic push
 #pragma GCC diagnostic ignored "-Wnon-virtual-dtor"
 
 class Kernel::Cpu : public Genode::Cpu, private Irq::Pool, private Timeout