diff options
| author | ppedrot | 2013-08-01 17:40:05 +0000 |
|---|---|---|
| committer | ppedrot | 2013-08-01 17:40:05 +0000 |
| commit | 88f8c20e3f55e8548d1f33b3407e68fb7dfb8317 (patch) | |
| tree | 2615bece9ef4fdae3f7528f3d43b2188aaa11011 /plugins/syntax | |
| parent | 8e88b7adab785146815e2fb25faf9b11fab989e8 (diff) | |
Added a test for bug #3088.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16650 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/syntax')
0 files changed, 0 insertions, 0 deletions