diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-11-23 10:55:32 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-11-23 10:57:10 +0100 |
commit | 7b3caccd054b6c912d4ded5c93d6b603c94904d2 (patch) | |
tree | d917d07e1ce497ca4ca557b9fcd01611fff1e1fe /checker/reduction.ml | |
parent | 7d541f25751838e1cde2a292a71afaa28879b753 (diff) |
Truncate strings in votour to 1024 characters.
Making it bigger is kind of useless, takes time and clutters the output for
no real advantage.
Diffstat (limited to 'checker/reduction.ml')
0 files changed, 0 insertions, 0 deletions