Index: tools/check-batch-cmd
===================================================================
--- tools/check-batch-cmd	(revision 10082)
+++ tools/check-batch-cmd	(revision 10083)
@@ -74,2 +74,3 @@
   else:
     main()
+