diff options
| author | Frédéric Besson | 2020-03-11 17:41:45 +0100 |
|---|---|---|
| committer | Frédéric Besson | 2020-03-11 17:41:45 +0100 |
| commit | af1b164b2a496d9c44b4b8648e37514b3def5b7a (patch) | |
| tree | d080aefbf0938f4670e97346b80d9c732b4b7340 /plugins/micromega/persistent_cache.ml | |
| parent | affb2fd89073accaa79ff6c2e468eb1bb9bd96bb (diff) | |
| parent | 8af9dbdcc27934deda35f6c8fbdecdfe869b09c5 (diff) | |
Merge PR #11754: [micromega] Add numerical compatibility layer.
Ack-by: SkySkimmer
Reviewed-by: fajb
Diffstat (limited to 'plugins/micromega/persistent_cache.ml')
| -rw-r--r-- | plugins/micromega/persistent_cache.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml index d5b28cb03e..4777b5e231 100644 --- a/plugins/micromega/persistent_cache.ml +++ b/plugins/micromega/persistent_cache.ml @@ -82,9 +82,9 @@ module PHashtable (Key : HashedType) : PHashtable with type key = Key.t = struct with Unix.Unix_error (_, _, _) -> () (* Here, this is really bad news -- - there is a pending lock which could cause a deadlock. - Should it be an anomaly or produce a warning ? - *); + there is a pending lock which could cause a deadlock. + Should it be an anomaly or produce a warning ? + *); ignore (lseek fd pos SEEK_SET) (* We make the assumption that an acquired lock can always be released *) |