On Fri, 14 Jun 2019, Uwe Brauer wrote: > > On Fri, 14 Jun 2019, Faheem Mitha wrote: > > DEB_BUILD_OPTIONS="nocheck" make deb > Bash or tcsh? I don't know about tcsh. But try it.