am 40ad715f: am 7fc13d7a: am 1cad9512: Merge "Fix repo script to ignore tools"

* commit '40ad715f74740451e888b336b302f9e8628f3964':
  Fix repo script to ignore tools