[Date Prev][Date Next] [Chronological] [Thread] [Top]

Re: [mizar] Private DB




Hi Adam, Freek,

Actually, there is a way to put the files generated by accommodation in a
folder different from TEXT - but not many people know it, only really old
users, I believe: one just adds a second parameter to Mizar utilities
apart from the *.miz file to process - that's the place where the
environment is supposed to be.

Hopefully this does not work any more (I tried "accom foo.miz env" - maybe an option is needed?).

So why isn't this in the manual? :-)

If it worked, and people used it with an arbitrary directory in shell, things would break afterwards in Emacs now. It's not a big deal though, and especially if there would be a default name of that directory (some "ENV", etc.). Still, such a change would be one of the most disruptive, outdating a lot of tools which no one cares to maintain. That's probably one of the strongest justifications of the conservative "if it works, don't touch it" :-).

Josef