diff options
| author | jp | 2020-02-12 22:53:39 +0000 |
|---|---|---|
| committer | jp | 2020-02-12 22:53:39 +0000 |
| commit | df6732cc2206e6a2918e04ebb15c04fbc7d91f57 (patch) | |
| tree | c892a695bfb4367c19a06c7a28fb9a83943a8cd3 /lib/hol | |
| parent | 49275011e172b8bb587a6e7f023deeac9343d8bb (diff) | |
add vscode syntax highlighting mode
Diffstat (limited to 'lib/hol')
0 files changed, 0 insertions, 0 deletions