diff options
| author | Mohammad Akhlaghi <mohammad@akhlaghi.org> | 2018-08-24 15:59:16 +0200 |
|---|---|---|
| committer | Mohammad Akhlaghi <mohammad@akhlaghi.org> | 2018-08-24 16:03:07 +0200 |
| commit | cfc133583d32f278b1b6486776273b6f07973947 (patch) | |
| tree | 5dde4d86a25767158e0fa64022e0fea3d6190d5f /reproduce/src/make/Top-Makefile | |
| parent | ea2af4b56aad2bff82a4e11a1aa3f980b8432340 (diff) | |
Step to check pipeline added in README.md checklist
A step was added close to the top of the checklist to remind people to
check the pipeline before making any changes. Also, the `--origin' option
was removed from the `git clone' command into a separate command to rename
the origin branch. This helps in readability.
Diffstat (limited to 'reproduce/src/make/Top-Makefile')
0 files changed, 0 insertions, 0 deletions