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

Re: [mizar] Private DB



On Mon, 18 Sep 2006, Josef Urban wrote:

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?).

Hopefully it does :-) Maybe I didn't explain it clearly - the second argument is not just the folder, but also the 'base name' of the environment files, so that files with various names can be kept there, e.g.

accom foo.miz env/foo

or even

accom foo.miz env/poo

I agree that the usefulness of this is rather restricted (we used it once for preparing teaching resources to share by several users) - it probably explains that the feature is not documented enywhere else but at the webpage http://mizar.uwb.edu.pl/system/accommodator.html and I wouldn't advocate for implementing it in Emacs.

Best,
Adam