diff options
Diffstat (limited to 'doc/changelog/03-notations/11986-float-low-level-printing.rst')
| -rw-r--r-- | doc/changelog/03-notations/11986-float-low-level-printing.rst | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/changelog/03-notations/11986-float-low-level-printing.rst b/doc/changelog/03-notations/11986-float-low-level-printing.rst index f3d85cadc6..aba74891c6 100644 --- a/doc/changelog/03-notations/11986-float-low-level-printing.rst +++ b/doc/changelog/03-notations/11986-float-low-level-printing.rst @@ -1,5 +1,5 @@ - **Added:** - Add flag ``Printing Float`` to print primitive floats as hexadecimal - instead of decimal values. This is included in ``Set Printing All``. + :flag:`Printing Float` flag to print primitive floats as hexadecimal + instead of decimal values. This is included in the :flag:`Printing All` flag (`#11986 <https://github.com/coq/coq/pull/11986>`_, by Pierre Roux). |