]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 14d838b) | patch
- get working directory from env var DRAW_GRAPH_DIR
authorStefano Zacchiroli <zack@upsilon.cc>
Wed, 20 Nov 2002 16:30:18 +0000 (16:30 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Wed, 20 Nov 2002 16:30:18 +0000 (16:30 +0000)
commit74b066524fed3d838137fd17c2abdb3d4544d824
tree27239a399945f19530f3d31413de791f0741870dtree | snapshot
parent14d838b61590fe8ee7a599013bab547a2e542ff3commit | diff
- get working directory from env var DRAW_GRAPH_DIR
- in case of make failure (which in turn usually depends on uwobo's
  failure) return an error message in HTML format
- bugfix: return html file instead of ... nothing :)
- bugfix: print real current directory
helm/graphs/tools/drawGraph.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.