diff --git a/platform/mbed_rtc_time.h b/platform/mbed_rtc_time.h
index 4ec9c328d2..f1b04c3d68 100644
--- a/platform/mbed_rtc_time.h
+++ b/platform/mbed_rtc_time.h
@@ -40,10 +40,10 @@ extern "C" {
  * int main() {
  *     set_time(1256729737);  // Set RTC time to Wed, 28 Oct 2009 11:35:37
  *
- *     while(1) {
+ *     while (true) {
  *         time_t seconds = time(NULL);
  *
- *         printf("Time as seconds since January 1, 1970 = %d\n", seconds);
+ *         printf("Time as seconds since January 1, 1970 = %u\n", (unsigned int)seconds);
  *
  *         printf("Time as a basic string = %s", ctime(&seconds));
  *