Browse Source

Avoid getting $BASH from the shell (/bin/sh, typically), we prefer to use /bin/bash for reproducibility

Samuel Thibault 6 years ago
parent
commit
420c3e1274
2 changed files with 3 additions and 3 deletions
  1. 1 1
      configure.ac
  2. 2 2
      tools/starpu_codelet_profile.in

+ 1 - 1
configure.ac

@@ -512,7 +512,7 @@ AC_HEADER_STDC
 AC_C_RESTRICT
 
 # Check if bash is available
-AC_CHECK_PROGS([BASH], [bash])
+AC_CHECK_PROGS([REALBASH], [bash])
 
 # Record git version
 AC_PATH_PROG(gitcommand, git)

+ 2 - 2
tools/starpu_codelet_profile.in

@@ -1,8 +1,8 @@
-#!@BASH@
+#!@REALBASH@
 # StarPU --- Runtime system for heterogeneous multicore architectures.
 #
 # Copyright (C) 2010,2013,2015,2017                      CNRS
-# Copyright (C) 2008-2011,2013,2014                      Université de Bordeaux
+# Copyright (C) 2008-2011,2013,2014,2018                 Université de Bordeaux
 #
 # StarPU is free software; you can redistribute it and/or modify
 # it under the terms of the GNU Lesser General Public License as published by