update

[l4.git] / kernel / fiasco / src / jdb / jdb_ipi.cpp

diff --git a/kernel/fiasco/src/jdb/jdb_ipi.cpp b/kernel/fiasco/src/jdb/jdb_ipi.cpp
index cde9d2b04d740ab4b9b588e50a772a7ef3b5c8d3..159849ab032c928687560ed730a7a97d2f7928a8 100644 (file)
--- a/kernel/fiasco/src/jdb/jdb_ipi.cpp
+++ b/kernel/fiasco/src/jdb/jdb_ipi.cpp
@@ -20,8 +20,9 @@ PRIVATE static
 void
 Jdb_ipi_module::print_info(unsigned cpu)
 {
+  Ipi &ipi = Ipi::cpu(cpu);
   printf("CPU%02u sent/rcvd: %ld/%ld\n",
-         cpu, Ipi::_stat_sent.cpu(cpu), Ipi::_stat_received.cpu(cpu));
+         cpu, ipi._stat_sent, ipi._stat_received);
 }
 
 PUBLIC