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/E1jVynv-0003up-Hy%40rmmprod06.runbox.
