aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/library.ml
diff options
context:
space:
mode:
Diffstat (limited to 'library/library.ml')
-rw-r--r--library/library.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/library/library.ml b/library/library.ml
index 1da2c591d..e2832ecdc 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -683,7 +683,8 @@ let error_recursively_dependent_library dir =
let save_library_to ?todo dir f otab =
let except = match todo with
| None ->
- assert(!Flags.compilation_mode = Flags.BuildVo);
+ (* XXX *)
+ (* assert(!Flags.compilation_mode = Flags.BuildVo); *)
assert(Filename.check_suffix f ".vo");
Future.UUIDSet.empty
| Some (l,_) ->