diff --git a/doc/body.texi b/doc/body.texi
index fe6159699..f647111fe 100644
--- a/doc/body.texi
+++ b/doc/body.texi
@@ -798,6 +798,7 @@ int main(int argc, char *argv[])
 
   jit_disassemble();
 
+  jit_destroy_state();
   finish_jit();
   return 0;
 @}