From 0f17fd8da489986abee3e4078365c0afbba6b0b7 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 13 Dec 2024 16:21:52 +0100 Subject: [PATCH] [build] Don't use -a option for lustre FS. --- Makefile | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Makefile b/Makefile index 6ffda3eacc84..8a58cd7b4bac 100644 --- a/Makefile +++ b/Makefile @@ -131,10 +131,10 @@ _build/default/theories_dune _build/default/ltac2_dune .dune-stamp: FORCE touch .dune-stamp theories/dune: .dune-stamp - cp -a _build/default/theories_dune $@ && chmod +w $@ + cp _build/default/theories_dune $@ && chmod +w $@ user-contrib/Ltac2/dune: .dune-stamp - cp -a _build/default/ltac2_dune $@ && chmod +w $@ + cp _build/default/ltac2_dune $@ && chmod +w $@ FORCE: ;