diff options
| author |  Stephane Glondu <steph@glondu.net> | 2008-08-08 15:29:35 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2008-08-08 15:42:41 +0200 |
| commit | 280b58b25462cd9f8e33f96ff76e84cf22eb465c (patch) | |
| tree | c99b7b8a18b2a53c20cd3f531d9a292cd172264d /debian/coqide.desktop | |
| parent | 9fd4621dcafc03b56c348a0342b2d172c065121d (diff) | |
Move patch-stamp as a prerequisite of configure-stamp
Diffstat (limited to 'debian/coqide.desktop')
0 files changed, 0 insertions, 0 deletions