| name: "devtools" | |
| description: | |
| "Subtree at third_party/devtools." | |
| third_party { | |
| identifier { | |
| type: "ChromiumVersion" | |
| value: "80.0.3987.162" # from https://chromereleases.googleblog.com/2020/03/stable-channel-update-for-desktop_31.html | |
| } | |
| identifier { | |
| type: "Git" | |
| value: "https://chromium.googlesource.com/devtools/devtools-frontend.git" | |
| version: "0d4095e47ca0e972e04efecf7772a8d12b60c665" | |
| # from https://chromium.googlesource.com/chromium/src/+/80.0.3987.162/DEPS#247 | |
| } | |
| last_upgrade_date { | |
| year: 2019 | |
| month: 12 | |
| day: 12 | |
| } | |
| } |