On zaterdag 30 mei 2020 10:07:09 CEST Marius Bakke wrote:
> I don't think passing -Denable_gui=OFF twice makes a difference.  Does
> it?

LOL, yeah, you are right. It doesn't. 

Here is a new patch.
-- 
Tom Zander