Automatically copy the User Guide from docs to resources only if it d…

…id not exist or was out of date in resources.
fjwright · Oct 29, 2023 · c868f94 · c868f94
1 parent 9dfd649
commit c868f94
Showing 1 changed file with 4 additions and 1 deletion.
diff --git a/docs/UserGuide-to-resources.bat b/docs/UserGuide-to-resources.bat
@@ -1 +1,4 @@
-copy docs\UserGuide.html resources\
+@echo off
+rem Copy file only if source time newer than destination time.
+rem No prompting to overwrite an existing destination file.
+xcopy docs\UserGuide.html resources\ /D /Y