diff options
| author | Paul Steckler | 2017-12-01 16:13:06 -0500 |
|---|---|---|
| committer | Paul Steckler | 2017-12-01 16:14:31 -0500 |
| commit | 2b4ed9b34e3852df7582f2a084274340113194e4 (patch) | |
| tree | c7ca2e22071dbfa36bbcc7c0a4d07a01c73b76ac /dev | |
| parent | 0048cbe810c82a775558c14cd7fcae644e205c51 (diff) | |
uninstall doc dir, not dev (which is not installed), #6007
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/build/windows/patches_coq/coq_new.nsi | 2 |
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 b88aa066d8..48f1d3759b 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" |