[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
Re: [mizar] Private DB
On Sun, 17 Sep 2006, Josef Urban wrote:
One even more painful thing to do (at least from the point of fixing a
lot of Mizar tools) would be to have additional ENV directory for all
the environment files produced by accommodation, which are illegable to
users and just make mess out of their clean TEXT directory.
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.
Regards,
Adam Naumowicz
======================================================================
Department of Applied Logic fax. +48 (85) 745-7662
Institute of Computer Science tel. +48 (85) 745-7559 (office)
University of Bialystok e-mail: adamn@mizar.org
Sosnowa 64, 15-887 Bialystok, Poland http://math.uwb.edu.pl/~adamn/
======================================================================