diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-03-16 00:53:57 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-03-16 15:13:39 +0100 |
| commit | efcff2e4ae6cabaf90fec1d5bd0cec0f5d4a3a4a (patch) | |
| tree | 445e4579c0d2916400088181f392b93185a35f85 /doc/tools | |
| parent | 1b462cfd2b03fa90e30b6d53de3adb33bc756eaf (diff) | |
[Sphinx] Better error message for coqtop errors
Diffstat (limited to 'doc/tools')
| -rw-r--r-- | doc/tools/coqrst/repl/coqtop.py | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/doc/tools/coqrst/repl/coqtop.py b/doc/tools/coqrst/repl/coqtop.py index d0e8d5733..efb5cb550 100644 --- a/doc/tools/coqrst/repl/coqtop.py +++ b/doc/tools/coqrst/repl/coqtop.py @@ -70,9 +70,12 @@ class CoqTop: """ # Suppress newlines, but not spaces: they are significant in notations sentence = re.sub(r"[\r\n]+", " ", sentence).strip() - # print("Sending {}".format(sentence)) self.coqtop.sendline(sentence) - output = self.next_prompt() + try: + output = self.next_prompt() + except: + print("Error while sending the following sentence to coqtop: {}".format(sentence)) + raise # print("Got {}".format(repr(output))) return output |