2013-04-29 13:13:42 +02:00
|
|
|
#!/usr/bin/env python
|
|
|
|
|
import py_compile
|
|
|
|
|
import os
|
|
|
|
|
import os.path
|
|
|
|
|
import sys
|
|
|
|
|
import shutil
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
src_file = sys.argv[1]
|
|
|
|
|
target_file = sys.argv[2]
|
|
|
|
|
|
|
|
|
|
(target_path , tail) = os.path.split( target_file )
|
|
|
|
|
if not os.path.exists( target_path ):
|
2013-08-26 13:56:42 +02:00
|
|
|
try:
|
|
|
|
|
os.makedirs( target_path )
|
|
|
|
|
except:
|
|
|
|
|
# When running with make -j 4 there might be a race to create this directory.
|
|
|
|
|
pass
|
2013-04-29 13:13:42 +02:00
|
|
|
|
|
|
|
|
shutil.copyfile( src_file , target_file )
|
2015-07-01 13:24:34 +02:00
|
|
|
shutil.copystat( src_file , target_file )
|
2013-04-29 13:13:42 +02:00
|
|
|
try:
|
|
|
|
|
py_compile.compile( target_file , doraise = True)
|
|
|
|
|
except Exception,error:
|
|
|
|
|
sys.exit("py_compile(%s) failed:%s" % (target_file , error))
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
sys.exit(0)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|