diff options
| author | Maxime Dénès | 2017-12-05 09:52:09 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-12-05 09:52:09 +0100 |
| commit | 04d5253b91f7567a09b950caa420b69fc34c0d0e (patch) | |
| tree | d601128f0ebe23f9ffce44949666ba2f8a3630a9 /dev | |
| parent | ecc56d61d2a6b281fe1581e36859158f3ad04fcd (diff) | |
| parent | 2b4ed9b34e3852df7582f2a084274340113194e4 (diff) | |
Merge PR #6302: Uninstall doc dir, not dev (which is not installed), fixes #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" |