diff options
| author | ppedrot | 2012-05-02 17:32:46 +0000 |
|---|---|---|
| committer | ppedrot | 2012-05-02 17:32:46 +0000 |
| commit | d7a2b59e79c79d13f0146c40076ff80835b3c49f (patch) | |
| tree | 9d92259da830942e78773032b255ade568ef58ea /scripts | |
| parent | fed7d0f693128ae2a7c19a519882f12f138d88b4 (diff) | |
Quick workaround to handle badly designed Sourceview package.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15270 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'scripts')
0 files changed, 0 insertions, 0 deletions