# HG changeset patch
# User wenzelm
# Date 1381176166 -7200
# Node ID 8f7061babae4721db469152c4ffaa5aa6524cf26
# Parent  da2e6282a4f51da43bdeda157c8f6c26ba769b29
proper NULL termination;

diff -r da2e6282a4f5 -r 8f7061babae4 Admin/Linux/Isabelle.c
--- a/Admin/Linux/Isabelle.c	Mon Oct 07 21:24:44 2013 +0200
+++ b/Admin/Linux/Isabelle.c	Mon Oct 07 22:02:46 2013 +0200
@@ -22,7 +22,7 @@
   char **cmd_line = NULL;
   int i = 0;
 
-  cmd_line = malloc(sizeof(char *) * argc);
+  cmd_line = malloc(sizeof(char *) * (argc + 1));
   if (cmd_line == NULL) fail("Failed to allocate command line");
 
   cmd_line[0] = malloc(strlen(argv[0]) + 5);
@@ -33,6 +33,8 @@
 
   for (i = 1; i < argc; i++) cmd_line[i] = argv[i];
 
+  cmd_line[argc] = NULL;
+
   execvp(cmd_line[0], cmd_line);
   fail("Failed to execute application script");
 }