fix filename of downloaded pdf files

services/web/app/views/project/editor/left-menu.jade

@@ -15,7 +15,7 @@ aside#left-menu.full-size(
 				| #{translate("source")}
 		li
 			a(
-				ng-href="{{pdf.url}}"
+				ng-href="{{pdf.downloadUrl || pdf.url}}"
 				target="_blank"
 				ng-if="pdf.url"
 			)

services/web/app/views/project/editor/pdf.jade

@@ -46,7 +46,7 @@ div.full-size.pdf(ng-controller="PdfController")
 			) {{ pdf.logEntries.errors.length + pdf.logEntries.warnings.length }}
 			
 		a(
-			ng-href="{{pdf.url}}"
+			ng-href="{{pdf.downloadUrl || pdf.url}}"
 			target="_blank"
 			ng-if="pdf.url"
 			tooltip="#{translate('download_pdf')}"

services/web/public/coffee/ide/pdf/controllers/PdfController.coffee

@@ -100,6 +100,7 @@ define [
 				qs_args = ("#{k}=#{v}" for k, v of qs)
 				$scope.pdf.qs = if qs_args.length then "?" + qs_args.join("&") else ""
 				$scope.pdf.url += $scope.pdf.qs
+				$scope.pdf.downloadUrl = "/Project/#{$scope.project_id}/output/output.pdf" + $scope.pdf.qs
 
 				fetchLogs(fileByPath['output.log'], fileByPath['output.blg'])