Fail: a way to check that a command is refused without blocking a script

 "Fail cmd" is similar to "Time cmd", but instead of printing the execution time,
 it reverse the exit status of cmd. "Fail cmd" is successful iff cmd has ended with
 an error. This was, we can demonstrate erroneous commands in a script for
 pedagogical or testing purpose without having to comment it in order to play the rest
 of the script in coqide/PG.

  Coq < Fail Foo.
  The command has indeed failed with message:
  => Error: Unknown command of the non proof-editing mode.

  Coq < Fail Check Prop.
  Prop
     : Type
  Error: The command has not failed !

 Two more remarks:
 - Fail doesn't catch anomalies.
 - Yes it it possible to write things like Fail Fail ... :-)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12981 85f007b7-540e-0410-9357-904b9bb8a0f7

0 files changed, 0 insertions, 0 deletions