diff options
author | Mohammad Akhlaghi <mohammad@akhlaghi.org> | 2019-03-28 11:51:37 +0000 |
---|---|---|
committer | Mohammad Akhlaghi <mohammad@akhlaghi.org> | 2019-03-28 11:57:58 +0000 |
commit | 27d3bb906b843a38c371e66372745095ccaceef6 (patch) | |
tree | 4e34fba4d0343f543d4eba1359920b4cc5f4b2cb /reproduce/src | |
parent | 98d31767a965ec75f4920b666f236cbb6baa91ab (diff) |
Configure script now has options
With the options, it is now possible to run the configure script more
easily after the initial run. The `--help' option provides a nice and
complete introduction along with a listing of the input options and the
`-j' option can be use to manually set the number of threads.
Diffstat (limited to 'reproduce/src')
0 files changed, 0 insertions, 0 deletions