Code

Redirect warnings to stderr#86

Code

Closed

dpwiz wants to merge 1 commit intoGaloisInc:masterGaloisInc/ivory:masterfrom dpwiz:warnings-stderrCopy head branch name to clipboard

+8-6

Commits

Commits on Oct 14, 2016

• Redirect warnings to stderr to prevent them from interfering with user out

  

  Alexander A Bondarenko

  authored and

  Alexander A Bondarenko

  committed
  0781bca