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

Re: [mizar] Private DB

To: mizar-forum@mizar.uwb.edu.pl
Subject: Re: [mizar] Private DB
From: Freek Wiedijk <freek@cs.ru.nl>
Date: Sun, 17 Sep 2006 14:50:30 +0200

Josef:

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

What I always want is to have all those files just be
combined into one _file_ (with separators in such a way that
it is easy to navigate that file, I guess.)  Is there a good
reason not to do this, apart from the fact that all the tools
will need to be changed for that?

Freek

Follow-Ups:
- Re: [mizar] Private DB
  - From: Andrzej Trybulec <trybulec@asuka.cs.shinshu-u.ac.jp>

References:
- Re: [mizar] Type extensions
  - From: Josef Urban <urban@ktilinux.ms.mff.cuni.cz>
- Re: [mizar] Type extensions
  - From: Andrzej Trybulec <trybulec@asuka.cs.shinshu-u.ac.jp>
- Re: [mizar] Type extensions
  - From: Artur Kornilowicz <arturk@math.uwb.edu.pl>
- Re: [mizar] Type extensions
  - From: Andrzej Trybulec <trybulec@asuka.cs.shinshu-u.ac.jp>
- [mizar] Private DB
  - From: Andrzej Trybulec <trybulec@asuka.cs.shinshu-u.ac.jp>
- Re: [mizar] Private DB
  - From: "Jesse Alama" <alama@stanford.edu>
- Re: [mizar] Private DB
  - From: Andrzej Trybulec <trybulec@asuka.cs.shinshu-u.ac.jp>
- Re: [mizar] Private DB
  - From: Josef Urban <urban@ktilinux.ms.mff.cuni.cz>
- Re: [mizar] Private DB
  - From: Andrzej Trybulec <trybulec@asuka.cs.shinshu-u.ac.jp>
- Re: [mizar] Private DB
  - From: Josef Urban <urban@ktilinux.ms.mff.cuni.cz>

Prev by Date: Re: [mizar] Private DB
Next by Date: Re: [mizar] Private DB
Index(es):
- Chronological
- Thread