diff -r 8b32fd4d0194 -r 668a54686827 main.cc
--- a/main.cc	Tue Aug 19 18:04:28 2008 +0200
+++ b/main.cc	Thu Aug 21 16:08:19 2008 +0200
@@ -61,7 +61,7 @@
 
 
 //#include <stdio.h>   // printf()
-
+#include <string.h>
 #include <stdlib.h>  // EXIT_FAILURE
 #include "absyntax/absyntax.hh"  // symbol_c type