diff options
| author | Enrico Tassi | 2014-12-19 17:32:03 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2014-12-19 17:47:50 +0100 |
| commit | b24741df01cd98dc63b6c4d43b11e6e38b44a887 (patch) | |
| tree | 3e520074fcd415f83a69db3db91b36fe17084f06 /dev | |
| parent | fb9815baafc008a6e67e542eb8c2adf7a6375fe8 (diff) | |
Install .v and .glob files too
PIDE based user interfaces use glob files and source files to
implement hyperlinks
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions