« Previous | Next » 

Revision f723de38

IDf723de389912545cb7b7e9966167c6baa80555aa
Parent b2278348
Child 2fe61f87

Added by Iustin Pop over 14 years ago

Improve the error message for command line errors

Instead of using ioError . userError, we format the error ourselves.
This is nicer - no ‘)’ at the end of the output.

Files

  • added
  • modified
  • copied
  • renamed
  • deleted

View differences