Rename badly named linuxHeaders_3_7 (it's actually 3.12)

This commit is contained in:
Eelco Dolstra
2014-10-29 13:43:00 +01:00
parent 5b50f0cbc5
commit 937e1280c0
2 changed files with 2 additions and 2 deletions