From 67829d634b885b5a7b353b4a5d7eac34d80d66a7 Mon Sep 17 00:00:00 2001
From: Holger Vogt <holger.vogt@uni-due.de>
Date: Tue, 30 Apr 2024 16:21:26 +0200
Subject: [PATCH] Don't delete sourceinfo as it may lead to a crash upon
 'quit'. Needs further investigation.

---
 src/frontend/misccoms.c | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/frontend/misccoms.c b/src/frontend/misccoms.c
index e3501b1d8..1ac669039 100644
--- a/src/frontend/misccoms.c
+++ b/src/frontend/misccoms.c
@@ -105,7 +105,7 @@ com_quit(wordlist *wl)
     pl_rempar();
 
     while (ft_curckt) {
-        wl_delete(ft_curckt->ci_sourceinfo);
+//        wl_delete(ft_curckt->ci_sourceinfo);
         com_remcirc(NULL);
     }
 #endif