diff --git a/share/libc/time.h b/share/libc/time.h
index 52c4455579fc3c1269c131021b2582575c5fd52e..ffe74960d94212f40e32a517a2904e5ff256bbc4 100644
--- a/share/libc/time.h
+++ b/share/libc/time.h
@@ -169,7 +169,7 @@ extern int clock_getres(clockid_t, struct timespec *);
 #else
     // simulates a system without monotonic clock
     assigns \result\from clk_id;
-    ensures error: \result == EINVAL
+    ensures error: \result == EINVAL;
 #endif
   behavior bad_clock_id:
     assumes bad_id: clk_id != CLOCK_REALTIME && clk_id != CLOCK_MONOTONIC;