aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/byterun/coq_memory.c
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/byterun/coq_memory.c')
-rw-r--r--kernel/byterun/coq_memory.c1
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c
index c9bcdc32f..45cfae509 100644
--- a/kernel/byterun/coq_memory.c
+++ b/kernel/byterun/coq_memory.c
@@ -130,6 +130,7 @@ value init_coq_vm(value unit) /* ML */
return Val_unit;;
}
+/* [required_space] is a size in words */
void realloc_coq_stack(asize_t required_space)
{
asize_t size;