diff options
| author | Alasdair | 2020-05-14 10:08:43 +0100 |
|---|---|---|
| committer | Alasdair | 2020-05-14 10:08:43 +0100 |
| commit | f05e81a641b4fb6f2d5e69ef4c13e0ada3dc3bfb (patch) | |
| tree | f7a57d9dcefb1924741ec710aee4d6d28a7d7892 /src | |
| parent | 0c4c75d13aad176fc664e159d2b0c48c77b41d27 (diff) | |
Attempt to fix CI error
Diffstat (limited to 'src')
| -rw-r--r-- | src/sail.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/sail.ml b/src/sail.ml index 8e89bbed..1f1b2489 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -55,7 +55,9 @@ module Json = Yojson.Basic let lib = ref ([] : string list) let opt_interactive_script : string option ref = ref None -let opt_config : Json.t option ref = ref None +(* Note: May cause a depcrecated warning for json type, but this cannot be + fixed without breaking Ubuntu 18.04 CI *) +let opt_config : Json.json option ref = ref None let opt_print_version = ref false let opt_target = ref None let opt_tofrominterp_output_dir : string option ref = ref None |
