diff options
Diffstat (limited to 'library/library.ml')
| -rw-r--r-- | library/library.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/library/library.ml b/library/library.ml index 6da9ccf68..024ac9e6f 100644 --- a/library/library.ml +++ b/library/library.ml @@ -768,7 +768,7 @@ let save_library_to ?todo dir f otab = iraise reraise let save_library_raw f sum lib univs proofs = - let f' = f^".o" in + let f' = f^"o" in let ch = raw_extern_library f' in System.marshal_out_segment f' ch (sum : seg_sum); System.marshal_out_segment f' ch (lib : seg_lib); |