aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Paul Steckler <steck@stecksoft.com>2017-12-01 16:13:06 -0500
committerGravatar Paul Steckler <steck@stecksoft.com>2017-12-01 16:14:31 -0500
commit2b4ed9b34e3852df7582f2a084274340113194e4 (patch)
treec7ca2e22071dbfa36bbcc7c0a4d07a01c73b76ac
parent0048cbe810c82a775558c14cd7fcae644e205c51 (diff)
uninstall doc dir, not dev (which is not installed), #6007
-rw-r--r--dev/build/windows/patches_coq/coq_new.nsi2
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/build/windows/patches_coq/coq_new.nsi b/dev/build/windows/patches_coq/coq_new.nsi
index b88aa066d..48f1d3759 100644
--- a/dev/build/windows/patches_coq/coq_new.nsi
+++ b/dev/build/windows/patches_coq/coq_new.nsi
@@ -188,7 +188,7 @@ SectionEnd
Section "Uninstall"
; Files and folders
RMDir /r "$INSTDIR\bin"
- RMDir /r "$INSTDIR\dev"
+ RMDir /r "$INSTDIR\doc"
RMDir /r "$INSTDIR\etc"
RMDir /r "$INSTDIR\lib"
RMDir /r "$INSTDIR\libocaml"