-------- Forwarded Message --------
Subject: Current problem
Date: Tue, 5 May 2020 20:19:24 +0200 (CEST)
From: fl
To: Megill Norman

 Hi Norm,

Can you post this.

I don't know how you do, but my own version of mmj2 has no problems to find 
set.mm in the current directory.

-- 
FL

On Tuesday, May 5, 2020 at 10:44:18 AM UTC-4, David A. Wheeler wrote:
>
> FL: 
> > For me it's not "/usr/bin" it's "/usr/local/bin" 
>
> That's true for many people. Metamath-exe actually already supports this, 
> just use "make install" with autoconf (as always that's the default). 
> If you want /usr/bin (as is common for packages installed with a 
> package manager), use "PREFIX=/usr/bin make install" 
>
> ... 
>
> > and set.mm is not a library it's a file of data. 
> > You have to be able to browse it and modify it with an editor. 
>
> Agreed. 
>
> > And the applications must look for it in the current directory "." not 
> in $HOME. 
>
> The bigger problem is mmj2. 
> GUIs don't really have the concept of "current directory", and mmj2 
> needs to know where its current database is. 
>
> --- David A. Wheeler

-- 
You received this message because you are subscribed to the Google Groups 
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to [email protected].
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/7f91a511-acb0-4cac-952a-9d11a31df858%40googlegroups.com.

Reply via email to