[antimicro/f20] Previous source used commit in directory name due to confusion w/ GitHub URL. Fixed.

[jsbackus]

Summary of changes:

  a20511b... Previous source used commit in directory name due to confus (*)

(*) This commit already existed in another branch; no separate mail sent