GNU bug report logs - #43248
[PATCH] Fix coqide

Previous Next

Full log

Message #10 received at 43248-done <at> debbugs.gnu.org (full text, mbox):

From: Julien Lepiller <julien <at> lepiller.eu>
To: raingloom <raingloom <at> riseup.net>
Cc: 43248-done <at> debbugs.gnu.org
Subject: Re: [bug#43248] [PATCH] Fix coqide
Date: Mon, 7 Sep 2020 14:03:23 +0200

Le Sun, 6 Sep 2020 20:02:03 +0200,
raingloom <raingloom <at> riseup.net> a écrit :

> coqide wasn't working because it couldn't find coqidetop.opt, because
> it was being deleted due to being a duplicate of coqidetop.
> 
> I looked at the source to figure out a way to simply convince Coq to
> use coqidetop, but it would have require too much patching, also other
> tools might assume either coqidetop or coqidetop.opt being available,
> so to be safe, I made one into a symlink to the other.
> 
> Coqide now works without any weird workarounds.

Pushed as 1394765238c21030ace4fbb773dc86a9e3c2504c, thank you!

Previous Next

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.