Merge branch 'main' into jca_signature_extensions

This commit is contained in:
Nicolas Will
2025-10-06 14:50:15 +02:00
committed by GitHub
218 changed files with 3106 additions and 2157 deletions

View File

@@ -87,6 +87,7 @@ class ElementBase extends @element {
*/
class Element extends ElementBase {
/** Gets the primary file where this element occurs. */
pragma[nomagic]
File getFile() { result = this.getLocation().getFile() }
/**