diff options
| author | charguer | 2019-11-08 11:06:10 +0100 |
|---|---|---|
| committer | charguer | 2019-11-20 12:02:00 +0100 |
| commit | 5bf25dfce23da1cee04b1c886e026f0dbc902c9c (patch) | |
| tree | 44258f30e5965dcfc1e316c4bd4812698dcf7777 /vernac/loadpath.ml | |
| parent | 64ddd9ac0c34e560a0640297e2e23b6aaf074810 (diff) | |
From CoqIDE or -vos or -vok compilation, load .vo when .vos is missing (fixing bug #11057).
With this new behavior, it is not needed to .vos files in user contribs.
Also, this commit adds a feature: upon creation of a .vo file, an empty .vok file is touched.
Diffstat (limited to 'vernac/loadpath.ml')
| -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 |