uint32_t type needed even if stats are not enabled.
commit1b7ce8002ac7eb90b5fe19a7934315d717e9d430
authorCalvin Beck <hobbes@ualberta.ca>
dateWed 25 Feb 2015, 21:42 (12 years ago)
parentb32de5c
rts/idris_stats.h+2−1
@@ -3,9 +3,10 @@
33
44#ifdef IDRIS_ENABLE_STATS
55#include <time.h>
6+#endif
7+
68#include <inttypes.h>
79#include <stdint.h>
8−#endif
910
1011
1112// TODO: measure user time, exclusive/inclusive stats