[PATCH 12/12 gnumach] Debug printf when sending TLB IPI

[Damien Zammit]

---
 i386/i386/smp.c | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/i386/i386/smp.c b/i386/i386/smp.c
index acf69d21..c6a62958 100644
--- a/i386/i386/smp.c
+++ b/i386/i386/smp.c
@@ -53,7 +53,7 @@ void smp_pmap_update(unsigned apic_id)

     cpu_intr_save(&flags);

-    printf("Sending IPI(%u) to call TLB shootdown...", apic_id);
+    printf("IPI(%d>%u)\n", cpu_number(), apic_id);
     apic_send_ipi(NO_SHORTHAND, FIXED, PHYSICAL, ASSERT, EDGE, 
CALL_SINGLE_FUNCTION_BASE, apic_id);

     do {
--
2.34.1