diff --git a/bin/frama-c b/bin/frama-c index 86398b26384daab1c1da65bfb4f7ba3e7f301a34..88838755bcbd17e06054b3cdd1f6666a0b0fc7c1 100755 --- a/bin/frama-c +++ b/bin/frama-c @@ -22,4 +22,4 @@ ########################################################################## -dune exec --root=$(dirname $0)/.. --no-build frama-c -- "$@" +dune exec --root=$(dirname $0)/.. --no-build --no-print-directory -- frama-c "$@"