diff options
| author | Johannes Schauer <josch@debian.org> | 2016-10-19 17:06:13 +0200 |
|---|---|---|
| committer | Johannes Schauer <josch@debian.org> | 2016-10-19 17:06:13 +0200 |
| commit | d357e9bad36ffd0c4d9db9a9d0693a45cc93cc45 (patch) | |
| tree | 123e994df6ac472768cdbfebbd67c9574fbe8ebf /graphmlReader.ml | |
| parent | e05709250e7b9463345e2b6a5247d021f7f48d5d (diff) | |
import upstream version 0.19
Diffstat (limited to 'graphmlReader.ml')
| -rw-r--r-- | graphmlReader.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/graphmlReader.ml b/graphmlReader.ml index d053ddf..182c5f7 100644 --- a/graphmlReader.ml +++ b/graphmlReader.ml @@ -10,7 +10,7 @@ (* library, see the COPYING file for more information. *) (**************************************************************************) -open ExtLib +open! ExtLib type value = | Int of int |