diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-09-29 21:27:26 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-09-29 21:27:26 +0200 |
| commit | 99918c8a8cfb4285798a70351673be2679a6e819 (patch) | |
| tree | d4a8682ac818432d4dfcbb454170f01dbe9c26c5 /library/library.ml | |
| parent | 05ab666a1283de5500dbc0520d18bdb05d95f286 (diff) | |
Fix dumb typo.
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); |