--- a/kernel/eka/nkern/arm/ncsched.cia	Tue Jun 15 13:29:38 2010 +0100
+++ b/kernel/eka/nkern/arm/ncsched.cia	Tue Jun 15 16:21:40 2010 +0100
@@ -1760,11 +1760,11 @@
 	SET_THUMB2EE_HNDLR_BASE(,r1);			
 #endif
 #ifdef __CPU_HAS_CP15_THREAD_ID_REG
-	SET_RWRW_TID(,r3)						// restore Thread ID from r3
+	SET_RWRW_TID(,r3);						// restore Thread ID from r3
 #endif 
 	asm("mov r3, r2 ");						// r3=TheCurrentThread
 #ifdef __CPU_HAS_COPROCESSOR_ACCESS_REG
-	SET_CAR(,r10)
+	SET_CAR(,r10);
 #endif
 #ifdef __CPU_ARM_USE_DOMAINS
 	asm("mcr p15, 0, r11, c3, c0, 0 ");