diff options
author | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-01-06 11:48:50 +0000 |
---|---|---|
committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-01-06 11:48:50 +0000 |
commit | eed2bb82eb4b97881f155079fd457a8de75bdba5 (patch) | |
tree | bdad1789ce20b86b58f2414ac7b80cbd959ea7c3 /config | |
parent | 12c796fe185876021e2dfc7753b8f90ba9de31e0 (diff) |
Remove Safe_marshal
Safe_marshal was using intermediate strings that are subject to
Sys.max_string_length limitation. Use directly binary channel-oriented
functions instead. This is a fix for bug #2471. Remark: this might
reduce robustness w.r.t. noise in the communication channel.
AFAIK, the original purpose of Safe_marshal was to work around a bug
on Windows... this should be investigated further.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13765 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'config')
0 files changed, 0 insertions, 0 deletions