Hi,

Il 12/07/20 19:28, David A. Wheeler ha scritto:
> Is your current plan to store them in:
> /usr/share/metamath-databases/
> ?

I would go for /usr/share/metamath/databases/, so that if in the future
metamath or other metamath-related programs have somthing to install, it
can go in /usr/share/metamath and only one direct child of /usr/share is
created for metamath.

>> I see that set.mm, iset.mm and nf.mm are
>> maintained in [1], which can be probably considered their canonical
>> location (using branch "develop")....
> 
> That seems reasonable for now. The branch name might change eventually,
> but that seems like the current one.

Not a problem. This is just for me to know where to take the files from.
The string "develop" doesn't go anywhere relevant in the Debian package.

Giovanni.
-- 
Giovanni Mascellani <[email protected]>
Postdoc researcher - Université Libre de Bruxelles

-- 
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/1d1ea2d6-5adf-776e-5d8b-682828f5344e%40gmail.com.

Attachment: signature.asc
Description: OpenPGP digital signature

Reply via email to