]> matita.cs.unibo.it Git - helm.git/commitdiff
projects / helm.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: dcfdf34)
Typo fixed.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 19 Jan 2004 14:26:46 +0000 (14:26 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 19 Jan 2004 14:26:46 +0000 (14:26 +0000)
helm/graphs/tools/drawGraph.ml patch | blob | history

diff --git a/helm/graphs/tools/drawGraph.ml b/helm/graphs/tools/drawGraph.ml
index 0714383190fbc4f75b4db18abf063ee1f25eaf59..dd0e6cf5c00b2bb93318a4f708333137c261112d 100644 (file)
--- a/helm/graphs/tools/drawGraph.ml
+++ b/helm/graphs/tools/drawGraph.ml
@@ -58,7 +58,7 @@ let errmsg =
   <title>Graph: error</title>
  </head>
  <body>
-  <h1>Error occured while drawing graph!<br />Please report the occured problem</h1>
+  <h1>Error occurred while drawing graph!<br />Please report the occured problem</h1>
   <h2>%s</h2>
  </body>
 </html>"
Unnamed repository; edit this file 'description' to name the repository.