Remove un-needed scripts
authorKim Nguyễn <kn@lri.fr>
Wed, 24 Jul 2013 21:50:43 +0000 (23:50 +0200)
committerKim Nguyễn <kn@lri.fr>
Wed, 24 Jul 2013 21:50:43 +0000 (23:50 +0200)
commit4cd6d4da36b7f61b8cd8a22d849590ed6143f2e7
tree3264bbe555fb6901f29a1a157d6f2ff9f990c504
parent2b85475321db7b38d4df0869fb51d38d98bb6671
Remove un-needed scripts
tools/odeps.sh [deleted file]
tools/osort.sh [deleted file]