Plugins: Include build number and PR in metadata (#18260)

2019-07-25 15:39:18 +02:00
parent 13c41b781a
commit 6fa617efdc
1 changed files with 2 additions and 0 deletions
@@ -82,6 +82,8 @@ export interface PluginBuildInfo {
  repo?: string;
  branch?: string;
  hash?: string;
+  number?: number;
+  pr?: string;
 }

 export interface PluginMetaInfo {