]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 347a0f4) | patch
Several changes:
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 15 May 2003 16:51:37 +0000 (16:51 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 15 May 2003 16:51:37 +0000 (16:51 +0000)
commit39c8c5c53680cd374a3eb76993a592cf29bb92ba
treeedd8072b830908f555dd7af0307c654c3574849ftree | snapshot
parent347a0f4a6e75a9c7dcef3c0f0da837c76c6e8890commit | diff
Several changes:

1. the UWOBO_LOG_FILE environment variable semantics changed. It is now
   used in the following way: $UWOBO_LOG_FILE.pid.log
2. when the log file can not be opened, UWOBO used to crash. Instead,
   it now goes on and a nice error message is printed on the stderr
   (but, unfortunately, it is not given back to the user, since the
   error is raised in a new process and it can not be read back from
   the logfile!)
helm/uwobo/uwobo.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.