projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 84146b4) | patch
push and pop manipulators for output stream so that one can indent the output
authorDejan Jovanović <dejan.jovanovic@gmail.com>
Thu, 17 Mar 2011 03:48:53 +0000 (03:48 +0000)
committerDejan Jovanović <dejan.jovanovic@gmail.com>
Thu, 17 Mar 2011 03:48:53 +0000 (03:48 +0000)
commitd0186bbce6187def699545d072bf2f95211398cc
treec0cd9df9b5698218cb2e973981dacd5c98b51d54tree
parent84146b42ed0e1c0298b0e2a894c33f357a4483efcommit | diff
push and pop manipulators for output stream so that one can indent the output
ueful for me, maybe someone else finds it useful also
src/util/output.h diff | blob | history