diff options
| author | alexwl <alexey.a.kiryushin@gmail.com> | 2018-11-30 14:20:41 +0300 |
|---|---|---|
| committer | alexwl <alexey.a.kiryushin@gmail.com> | 2018-11-30 14:20:41 +0300 |
| commit | 2c089ff24c85faf0595a1d8b985c4e3ead3f4b64 (patch) | |
| tree | 23ecc02b30dee2ac9cfe4e26ae5c7a60fd42ec3c /javascript/app/utils | |
| parent | 868b51bc5e26df88696e782c131d3fc47995facb (diff) | |
Show 'No location info' message for Paths_* modules
Diffstat (limited to 'javascript/app/utils')
| -rw-r--r-- | javascript/app/utils/go-to-definition.js | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/javascript/app/utils/go-to-definition.js b/javascript/app/utils/go-to-definition.js index 7063ec0..6eac9c3 100644 --- a/javascript/app/utils/go-to-definition.js +++ b/javascript/app/utils/go-to-definition.js @@ -41,7 +41,8 @@ function goToDefinition(store,locationInfo,buttonId,currentLineNumber) { saveCurrentLocation(currentLineNumber); } openUrl(buttonId,url); - } else if(locationInfo.tag === "ApproximateLocation") { + } else if((locationInfo.tag === "ApproximateLocation") && + (locationInfo.moduleName.indexOf("Paths_") !== 0)) { const packageId = locationInfo.packageId.name+"-"+locationInfo.packageId.version; if(locationInfo.entity === "Mod") { store.loadDefinitionSite(packageId, |