diff options
| author | Hendrik Tews | 2013-07-11 20:56:18 +0000 |
|---|---|---|
| committer | Hendrik Tews | 2013-07-11 20:56:18 +0000 |
| commit | 75770f871512bc094675b472fea9d8e086360484 (patch) | |
| tree | dc22a760069f8fc170b75a48fa50df11e7bbb340 /pgshell | |
| parent | a21fea06fb43db947427df6e91f32207aa64d596 (diff) | |
fix two bugs in parallel compilation for Coq
Diffstat (limited to 'pgshell')
0 files changed, 0 insertions, 0 deletions