diff options
| author | letouzey | 2010-03-04 16:18:11 +0000 |
|---|---|---|
| committer | letouzey | 2010-03-04 16:18:11 +0000 |
| commit | b1edecb1b38df8a88552aa4251982238b3c3125d (patch) | |
| tree | 5389cb05198071483d7cad7771b638d7a780a5b9 /plugins/syntax | |
| parent | 139bf11029dc16bf95c56646c41457b14cc35fdc (diff) | |
Makefile: make devdocclean was not removing *.dep.ps, btw let's remove *.dep.ps for svn
the syntax for find is sooo intuitive ...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12835 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/syntax')
0 files changed, 0 insertions, 0 deletions