Commit 11e805d39701513f7fdb3b692beb7c493a498a97

Patrick Monnerat 2015-04-17T17:02:59

xmllint: flush stdout before interactive shell input.