Merge branch 'extraction-create-prefix-paths-of-files' into 'master'
commit3fe04d2d4e2919197996a3f13338c4c24ff62298
authorJean-Christophe Filliâtre <jean-christophe.filliatre@inria.fr>
Tue, 7 May 2024 08:58:31 +0000 (7 10:58 +0200)
committerJean-Christophe Filliâtre <jean-christophe.filliatre@inria.fr>
Tue, 7 May 2024 08:58:31 +0000 (7 10:58 +0200)
tree15447c8daeb7af32e253490804812f5e6761048c
parent2c6eb2efaec6fe27f146dd80901182b71efef151
parent22d19d7401d72a96b35db87ae3aeb457abcac52d
Merge branch 'extraction-create-prefix-paths-of-files' into 'master'

chg: create path of output files

See merge request why3/why3!908