diff --git a/shell/cmd_time.c b/shell/cmd_time.c
index 47b3c1cb15a5a35afaf17b1ec01386dd93dbf1d8..8b79d1a39cf877d9a9a7e2afc4f4e5e85a673fc1 100644
--- a/shell/cmd_time.c
+++ b/shell/cmd_time.c
@@ -31,11 +31,11 @@ int cmd_time(const char *args[])
 			return -EBUSY;
 	} else if(args[0] && !strcasecmp(args[0], "raw"))
 	{
-			mprintf("%d %d\n", sec, nsec);
+			mprintf("%d %d\n", (uint32_t)sec, nsec);
 			return 0;
 	}
 
 	mprintf("%s +%d nanoseconds.\n", format_time(sec), nsec); /* fixme: clock freq is not always 125 MHz */
 	
 	return 0;	
-}
\ No newline at end of file
+}