diff options
| author | Masaya Tojo <masaya@tojo.tokyo> | 2021-08-29 22:10:18 +0900 |
|---|---|---|
| committer | Masaya Tojo <masaya@tojo.tokyo> | 2021-08-29 22:12:24 +0900 |
| commit | 59c353833fe0fed9af054b1557e63d6235485af7 (patch) | |
| tree | 8e9d6de13ce4356df6edb910171af9f8dcf6a4d3 /.gitignore | |
| parent | 9c084f62ea005299eba514bdeda799d3bf48188a (diff) | |
acl2: Remove -j option from make.
Diffstat (limited to '.gitignore')
0 files changed, 0 insertions, 0 deletions