diff options
| author | Hugo Herbelin | 2020-05-28 16:46:07 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-05-28 17:02:55 +0200 |
| commit | 5e0907df8a8711dcdbe92dc3a34225d32b300d0b (patch) | |
| tree | 51c567d074dc0c7028a7e4c188650fccfb3cfaaa /vernac/mltop.ml | |
| parent | a102a80d886bafc75991a446d1c1ae4c04494666 (diff) | |
Fixing compilation with -natdynlink no.
This complements #11407 about storing digests of modules.
Diffstat (limited to 'vernac/mltop.ml')
| -rw-r--r-- | vernac/mltop.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/vernac/mltop.ml b/vernac/mltop.ml index d276a1ac35..c33b3d29f8 100644 --- a/vernac/mltop.ml +++ b/vernac/mltop.ml @@ -309,6 +309,9 @@ type ml_module_object = { } let add_module_digest m = + if not has_dynlink then + m, NoDigest + else try let file = file_of_name m in let path, file = System.where_in_path ~warn:false !coq_mlpath_copy file in |