diff options
| author | Emilio Jesus Gallego Arias | 2019-12-09 14:49:42 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-12-13 17:05:48 +0100 |
| commit | 1e0c092e5856d9dbf4a009ef700549e58bbd76e5 (patch) | |
| tree | d5cf7d69e0f06811ed44a145baea36c679966814 /dev | |
| parent | a07480b5150d23b89a2a9acc09c8e506db9e73da (diff) | |
[make] Rename Makefile to Makefile.make
Picked from #8729. This should help preserve the history better when
we split.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions