diff options
| author | Pierre Courtieu | 2013-07-11 16:01:16 +0000 |
|---|---|---|
| committer | Pierre Courtieu | 2013-07-11 16:01:16 +0000 |
| commit | a21fea06fb43db947427df6e91f32207aa64d596 (patch) | |
| tree | 6c1a18061068e9b84bae63fd6bd24a9edcb0bc11 /pgshell/example.pgsh | |
| parent | 5cd9adb60e8b6e5fd1ce87adcf263c3a8b358cdc (diff) | |
Fixing a big bug in coq project file management.
file and directory name were not adapted to where the current file is
inside the directory structure. Now the absolute names are build.
Diffstat (limited to 'pgshell/example.pgsh')
0 files changed, 0 insertions, 0 deletions