Release docs build target

Author: wallymathieu

build.proj

@@ -20,12 +20,22 @@
 
   <!-- dotnet msbuild -target:AllDocs build.proj -->
   <Target Name="AllDocs">
+    <Exec Command='dotnet tool restore' WorkingDirectory="$(RepoRootDir)" IgnoreStandardErrorWarningFormat="true" />
     <Exec Command='dotnet build FSharpPlus.sln -c Release' WorkingDirectory="$(RepoRootDir)" IgnoreStandardErrorWarningFormat="true" />
     <Exec Command='./docsrc/tools/download_nugets.cmd' WorkingDirectory="$(RepoRootDir)" IgnoreStandardErrorWarningFormat="true" Condition=" '$(OS)' == 'Windows_NT' " />
     <Exec Command='./docsrc/tools/download_nugets.sh' WorkingDirectory="$(RepoRootDir)" IgnoreStandardErrorWarningFormat="true" Condition=" '$(OS)' != 'Windows_NT' " />
     <Exec Command='dotnet run -c Release --project ./docsrc/tools' WorkingDirectory="$(RepoRootDir)" IgnoreStandardErrorWarningFormat="true" />
   </Target>
 
+  <Target Name="ReleaseDocs">
+    <Exec Command='dotnet tool restore' WorkingDirectory="$(RepoRootDir)" IgnoreStandardErrorWarningFormat="true" />
+    <Exec Command='dotnet build FSharpPlus.sln -c Release' WorkingDirectory="$(RepoRootDir)" IgnoreStandardErrorWarningFormat="true" />
+    <Exec Command='./docsrc/tools/download_nugets.cmd' WorkingDirectory="$(RepoRootDir)" IgnoreStandardErrorWarningFormat="true" Condition=" '$(OS)' == 'Windows_NT' " />
+    <Exec Command='./docsrc/tools/download_nugets.sh' WorkingDirectory="$(RepoRootDir)" IgnoreStandardErrorWarningFormat="true" Condition=" '$(OS)' != 'Windows_NT' " />
+    <Exec Command='dotnet run -c Release --project ./docsrc/tools ReleaseDocs' WorkingDirectory="$(RepoRootDir)" IgnoreStandardErrorWarningFormat="true" />
+  </Target>
+
+
   <Target Name="VSTest" DependsOnTargets="Test" />
 
 </Project>

docsrc/tools/download_nugets.cmd

@@ -1,2 +1 @@
-@ECHO OFF
-PowerShell.exe -Command "& '%~dpn0.ps1'"
+@%SYSTEMROOT%\System32\WindowsPowerShell\v1.0\powershell.exe -ExecutionPolicy Bypass -Command "try { & '%~dpn0.ps1' %*; $err = -not $? } catch { Write-Host $_; $err = $true; $LastExitCode = 1 }; if ($err) { $ppid = (gwmi Win32_Process -Filter processid=$pid).ParentProcessId; $cl = (gwmi Win32_Process -Filter processid=$ppid).CommandLine; if ($cl -like '*cmd.exe /c*') { $gppid = (gwmi Win32_Process -Filter processid=$ppid).ParentProcessId; $pn = (gps -id $gppid).ProcessName; if ($pn -eq 'explorer') { pause } } }; exit $LastExitCode"