@@ -29,7 +29,9 @@ error(s,a) char *s,*a; {
fprintf(stderr,": ");
fprintf(stderr,s,a);
fprintf(stderr,"\n");
+#ifndef NDEBUG
abort();
+#endif
exit(-1);
}