tree 1c516dd4d561e9a71ea1fc8b9b6527b78cff0d21
parent 0d1c29a65872cb08d3e11df2c60aad6584e5b228
parent e98fa3a3c20584c48b3826fc6ad255a0bcfa6136
author davidcunado-arm <david.cunado@arm.com> 1492032224 +0100
committer GitHub <noreply@github.com> 1492032224 +0100

Merge pull request #885 from antonio-nino-diaz-arm/an/console-flush

Implement console_flush()