diff options
| author | Pierre Courtieu | 2015-11-12 13:36:24 +0100 |
|---|---|---|
| committer | Pierre Courtieu | 2015-11-12 13:36:24 +0100 |
| commit | 447a6c87348358acd9077d2898d858c0368d3ae8 (patch) | |
| tree | 50e8209b68322276b2b18240dd9d77e19466bf55 /isar/Example.thy | |
| parent | 8260bc52e829f21a664c13c4b1c5b70a8b0ee048 (diff) | |
Debuging: display a warning.
The warning is displayed when failing to retrieve last prompt info. Once
we understand what happened we can remove this warning.
Diffstat (limited to 'isar/Example.thy')
0 files changed, 0 insertions, 0 deletions