diff options
| author | Emilio Jesus Gallego Arias | 2019-11-21 11:05:00 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-11-21 11:05:00 +0100 |
| commit | b233d38a7a6a3e73f093c5c5ec00f1a7582e7668 (patch) | |
| tree | 3467207f621885afcaf131295d5516dfe38ae53b /vernac | |
| parent | e687dd9b1ee68b4ae00461a379a5207d6187a6d1 (diff) | |
| parent | 5bf25dfce23da1cee04b1c886e026f0dbc902c9c (diff) | |
Merge PR #11075: load .vo when .vos is missing + misc vos changes
Reviewed-by: gares
Reviewed-by: silene
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/loadpath.ml | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/vernac/loadpath.ml b/vernac/loadpath.ml index b3dc254a63..a8462e31e1 100644 --- a/vernac/loadpath.ml +++ b/vernac/loadpath.ml @@ -140,12 +140,10 @@ let select_vo_file ~warn loadpath base = with Not_found -> None in if !Flags.load_vos_libraries then begin (* If the .vos file exists and is not empty, it describes the library. - If the .vos file exists and is empty, then load the .vo file. - If the .vos file is missing, then fail. *) + Otherwise, load the .vo file, or fail if is missing. *) match find ".vos" with - | None -> Error LibNotFound - | Some (_, vos as resvos) -> - if (Unix.stat vos).Unix.st_size > 0 then Ok resvos else + | Some (_, vos as resvos) when (Unix.stat vos).Unix.st_size > 0 -> Ok resvos + | _ -> match find ".vo" with | None -> Error LibNotFound | Some resvo -> Ok resvo |