diff options
| author | Hugo Herbelin | 2020-12-18 18:57:25 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-12-18 18:57:25 +0100 |
| commit | 74ccd947d89e61ca1fc61575fe8012c2f8bd55fd (patch) | |
| tree | 86fcb2a3e4cf7823e094f734509401a46d0fc1ea /dev | |
| parent | 82d0a578b91f4de87deebc658b0e085646ca63d4 (diff) | |
Fixes #13657: vscoq needs goal uid.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions