From 5e0907df8a8711dcdbe92dc3a34225d32b300d0b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 28 May 2020 16:46:07 +0200
Subject: Fixing compilation with -natdynlink no.

This complements #11407 about storing digests of modules.
---
 vernac/mltop.ml | 3 +++
 1 file changed, 3 insertions(+)

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
-- 
cgit v1.2.3