./scripts/buildscript depends on bash

[Rafael Ávila de Espíndola <rafael.espindola@ic.unicamp.br>]

the buildscript uses pushd that isn't available in dash. Perhaps the first 
line should read "#/bin/bash"?

Thanks,
Rafael