Merge branch 'improve-error-message-on-unknown-module' into 'master'853-improve-documentation-of-extraction-to-c1069/head
| commit | 7e935097a6373f9843df3cfc9c3059c0ab40098e | |
| author | Jean-Christophe Filliâtre <jean-christophe.filliatre@inria.fr> | |
| Tue, 7 May 2024 11:08:36 +0000 (7 13:08 +0200) | ||
| committer | Jean-Christophe Filliâtre <jean-christophe.filliatre@inria.fr> | |
| Tue, 7 May 2024 11:08:36 +0000 (7 13:08 +0200) | ||
| tree | 32633a67cf8fd1c8847121a08fffeadefe6a49cc | treesnapshot (tar.gz zip) |
| parent | 3fe04d2d4e2919197996a3f13338c4c24ff62298 | commitdiff |
| parent | 32304b583f499ad2c588065d794ad9d59482374b | commitdiff |
Merge branch 'improve-error-message-on-unknown-module' into 'master'
chg: improve the error message when the specified module is not found
See merge request why3/why3!907
chg: improve the error message when the specified module is not found
See merge request why3/why3!907
| src/tools/why3extract.ml | diff1 | diff2 | blobhistory |