On Wed, 6 May 2020 00:45:22 -0700 (PDT), "'B. Wilson' via Metamath" <[email protected]> wrote: > Would it make sense to have "search path" variables for metamath and mmj2?
It could. All Metamath tools (at least Metamath & mmj2) would have to be modified to support it, and that's a minor pain. But once done things would "just work" even when people make a few different decisions, and that's an advantage. Here's a try: "METAMATHDB_PATH", if present, is a list of directories to be searched when a Metamath database is to be loaded and the database name does not include a directory separator. This modified name is from then on considered its name (e.g., if it is saved, then it saved to that location unless a different location is specified). The list uses the OS's standard format (; separated for Windows, : for everything else). On POSIX systems, the default value of METAMATHDB_PATH is: .:$HOME/set.mm:$HOME/metamath:/usr/var/metamath On Windows systems, the default value of METAMATHDB_PATH is: .;%USERPROFILE%\set.mm;%USERPROFILE%\metamath;%HOMEDRIVE%\set.mm;%HOMEDRIVE%\metamath;%SystemDrive%\Users\Public\metamath I'm not sure what a reasonable "global" value on Windows would be, so I used \Users\Public\metamath Note that in Windows, both "/" and "\" are directory separators. --- 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/E1jWNL0-0008Uy-Fe%40rmmprod06.runbox.
