Changeset 85221

Timestamp:

Aug 6, 2013, 1:36:38 PM (9 years ago)

Author:

Hartmut Kaiser

Message:

Fixed #8970: Karma fails to output a sign with a user-defined real number policy

(No files)