summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/sail.ml4
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