--- fiasco-1.0/l4/kernel/fiasco/src/kern/thread-syscall.cpp	Fri Mar 21 08:22:22 2003
+++ fiasco-patches/l4/kernel/fiasco/src/kern/thread-syscall.cpp	Thu Apr  3 13:08:18 2003
@@ -48,7 +48,7 @@
     printf("syscall number is %d\n", number);
   result = (t->*(syscall_table[number]))(static_cast<Syscall_frame *>(regs));
 
-#ifdef CONFIG_IA32
+#if defined(CONFIG_IA32) || defined(CONFIG_UX)
   regs->eax = result;
 #endif
   Proc::cli();