Add stdint.h header
I didn't need this locally, but perhaps it is necessary on other
platforms for uint8_t
commit9302ac5d01d46fd9547d4cdf0e4090f5e58c12ae
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateSat 25 Mar 2017, 21:06 (10 years ago)
parent3629548
rts/idris_buffer.h+1
@@ -3,6 +3,7 @@
33
44#include <stdlib.h>
55#include <stdio.h>
6+#include <stdint.h>
67
78void* idris_newBuffer(int bytes);
89