diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/sail.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/sail.ml b/src/sail.ml index 1f1b2489..9dbd1f6c 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -55,7 +55,7 @@ module Json = Yojson.Basic let lib = ref ([] : string list) let opt_interactive_script : string option ref = ref None -(* Note: May cause a depcrecated warning for json type, but this cannot be +(* Note: May cause a deprecated 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 |