diff options
| author | Filip Strömbäck <filip.stromback@liu.se> | 2018-04-18 17:41:11 +0200 |
|---|---|---|
| committer | Filip Strömbäck <filip.stromback@liu.se> | 2018-04-18 17:41:11 +0200 |
| commit | 6ca20446c77fd6dec9ca10713a63233c97e7e977 (patch) | |
| tree | 5a13f8923129321a6cab92ebe90399814da3adb5 /src/Make.config | |
| parent | f3e1dd764327c4d5361880c546bfa76baa97d32e (diff) | |
| download | pintos-rs-6ca20446c77fd6dec9ca10713a63233c97e7e977.tar.gz | |
Output the Pintos command line once more.
Signed-off-by: Filip Strömbäck <filip.stromback@liu.se>
Diffstat (limited to 'src/Make.config')
0 files changed, 0 insertions, 0 deletions