Index: kernel/arch/ia64/src/ski/ski.c
===================================================================
--- kernel/arch/ia64/src/ski/ski.c	(revision df4ed852a2d1b242f9bdce0a873009a2cb77cec7)
+++ kernel/arch/ia64/src/ski/ski.c	(revision 0f3fc9b4dfadc676e3337514570c32d8d8c9b162)
@@ -70,5 +70,5 @@
 void ski_putchar(chardev_t *d, const char ch)
 {
-	__asm__ volatile (
+	asm volatile (
 		"mov r15 = %0\n"
 		"mov r32 = %1\n"	/* r32 is in0 */
@@ -96,5 +96,5 @@
 	uint64_t ch;
 	
-	__asm__ volatile (
+	asm volatile (
 		"mov r15 = %1\n"
 		"break 0x80000;;\n"	/* modifies r8 */
@@ -205,5 +205,5 @@
 void ski_init_console(void)
 {
-	__asm__ volatile (
+	asm volatile (
 		"mov r15 = %0\n"
 		"break 0x80000\n"