From bf2400fd98cd025c360f6e28e32d36ed15ab6fde Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Patrick=20L=C3=BChne?= <patrick-github@luehne.de>
Date: Fri, 26 Jan 2018 18:47:11 +0100
Subject: [PATCH] Print statistics on SIGINT

---
 main.c | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/main.c b/main.c
index 1c74dc7..b17a9ae 100644
--- a/main.c
+++ b/main.c
@@ -268,7 +268,15 @@ void printStatistics()
   printf("...\n");
 }
 
+void handleSIGINT()
+{
+  printStatistics();
+  exit(0);
+}
+
 int main(int argc,char **argv) {
+  signal(SIGINT, handleSIGINT);
+
   int i,j;
 
   syntacticclass sclass;