add pid to temp filename so that make -j works
This commit is contained in:
parent
d70e53f243
commit
4c4f3b624d
@ -648,8 +648,9 @@ def gecode_version():
|
|||||||
import os
|
import os
|
||||||
cxx = new_compiler()
|
cxx = new_compiler()
|
||||||
customize_compiler(cxx)
|
customize_compiler(cxx)
|
||||||
file_hh = "_gecode_version.hh"
|
pid = os.getpid()
|
||||||
file_txt = "_gecode_version.txt"
|
file_hh = "_gecode_version_%d.hh" % pid
|
||||||
|
file_txt = "_gecode_version_%d.txt" % pid
|
||||||
f = file(file_hh,"w")
|
f = file(file_hh,"w")
|
||||||
f.write("""#include "gecode/support/config.hpp"
|
f.write("""#include "gecode/support/config.hpp"
|
||||||
@@GECODE_VERSION""")
|
@@GECODE_VERSION""")
|
||||||
|
Reference in New Issue
Block a user