[WINDOWS] remove complicated dos batch script that sometimes fails (#20670)

This commit is contained in:
Matti Picus 2021-11-23 18:59:29 +02:00 committed by GitHub
parent 2b5ad4a3c0
commit 85519fc3f6
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23

View file

@ -101,7 +101,6 @@ def copy_to_workspace(name, srcs, dstdir = ""):
name = name, name = name,
srcs = srcs, srcs = srcs,
outs = [name + ".out"], outs = [name + ".out"],
# Keep this Bash script equivalent to the batch script below (or take out the batch script)
cmd = r""" cmd = r"""
mkdir -p -- {dstdir} mkdir -p -- {dstdir}
for f in {locations}; do for f in {locations}; do
@ -113,20 +112,6 @@ def copy_to_workspace(name, srcs, dstdir = ""):
locations = src_locations, locations = src_locations,
dstdir = "." + ("/" + dstdir.replace("\\", "/")).rstrip("/") + "/", dstdir = "." + ("/" + dstdir.replace("\\", "/")).rstrip("/") + "/",
), ),
# Keep this batch script equivalent to the Bash script above (or take out the batch script)
cmd_bat = """
(
if not exist {dstdir} mkdir {dstdir}
) && (
for %f in ({locations}) do @(
(if exist {dstdir}%~nxf del /f /q {dstdir}%~nxf) &&
copy /B /Y %f {dstdir} >NUL
)
) && >$@ echo %TIME%
""".replace("\r", "").replace("\n", " ").format(
locations = src_locations,
dstdir = "." + ("\\" + dstdir.replace("/", "\\")).rstrip("\\") + "\\",
),
local = 1, local = 1,
tags = ["no-cache"], tags = ["no-cache"],
) )