Commit aae17f71 authored by Idir Lankri's avatar Idir Lankri

Prevent Git from detecting spurious changes in the repository

To do that, we use 'cp' instead of 'mv' when we want to move files
inside the repository.
parent c2e74853
......@@ -369,7 +369,7 @@ all: ZEN
cp -Rp $(MW) . # local copy of MW
# cd ML && $(MAKE) depend # reset dependencies (might be partial subset)
test -e ML/SCLpaths.ml && echo "SCL config detected" \
|| mv SETUP/dummy_SCLpaths.ml ML/SCLpaths.ml
|| cp SETUP/dummy_SCLpaths.ml ML/SCLpaths.ml
cd ML && $(MAKE) test_version
ML/test_stamp
cd ML && $(MAKE) # make engine (testing the data stamp)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment