git.annexia.org / goals.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: b889079) | patch
run: Improve consistency of error messages.
authorRichard W.M. Jones <rjones@redhat.com>
Fri, 10 Jan 2020 19:43:17 +0000 (19:43 +0000)
committerRichard W.M. Jones <rjones@redhat.com>
Fri, 10 Jan 2020 19:44:33 +0000 (19:44 +0000)
commit04ecb1624f8be51e1960c77d58036c480e93ed6b
treef492058fa134d22db130d32e1c34ad16d0a56582tree | snapshot
parentb8890796f260449084d5be3c036f9c479c38a5cecommit | diff
run: Improve consistency of error messages.

Make sure we always print the line number and the full name + params
of any goal or tactic which fails.
src/run.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.