3 commits

Author	SHA1	Message	Date
Sönke Hahn	b1d39d4765	dev-shell is a bash script, not sh ... 'type -p' does not work in e.g. dash	2014-05-26 17:21:20 +02:00
Eelco Dolstra	25a108bb9c	Hack to clean up tests/test-tmp	2013-08-21 12:53:46 +02:00
Eelco Dolstra	7b09e9f2c4	Add hacking notes plus a script for running nix-shell	2013-07-19 16:51:31 +02:00