diff options
| author | Nadrieril | 2019-04-07 14:17:38 +0200 |
|---|---|---|
| committer | Nadrieril | 2019-04-07 14:17:38 +0200 |
| commit | 0f5b69ac599a4b6979de465cf520ff5c283cfdbd (patch) | |
| tree | 3515e37af3a506a3ac1394c483802c1d49374e1e /.gitignore | |
| parent | d454d31ea07b70ff6d3f8d4d1014d37d954241dd (diff) | |
Use macros in typecheck; much cleaner
Diffstat (limited to '.gitignore')
0 files changed, 0 insertions, 0 deletions