patch-asrun_config.py

--- asrun/config.py.orig	2017-07-13 07:40:52 UTC
+++ asrun/config.py
@@ -44,8 +44,8 @@ DEFAULTS = {
     'SRCHIST'         : ['histor'],
     # name of "binaries" (as results of a make)
     'MAKE'            : ['debug nodebug'],
-    'BIN_NODBG'       : ['asteru.exe'],
-    'BIN_DBG'         : ['asterd.exe'],
+    'BIN_NODBG'       : ['asteru'],
+    'BIN_DBG'         : ['asterd'],
     'BINCMDE'         : ['commande'],
     'BINELE'          : ['elements'],
     'BINPICKLED'      : ['cata_ele.pickled'],