From: Claudio Sacerdoti Coen Date: Mon, 19 Jan 2004 14:26:46 +0000 (+0000) Subject: Typo fixed. X-Git-Tag: V_0_5_1_3~22 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=adb87d5ebd0149970fd45ce4976d4e0e058fb227;p=helm.git Typo fixed. --- diff --git a/helm/graphs/tools/drawGraph.ml b/helm/graphs/tools/drawGraph.ml index 071438319..dd0e6cf5c 100644 --- a/helm/graphs/tools/drawGraph.ml +++ b/helm/graphs/tools/drawGraph.ml @@ -58,7 +58,7 @@ let errmsg = Graph: error -

Error occured while drawing graph!
Please report the occured problem

+

Error occurred while drawing graph!
Please report the occured problem

%s

"