equal
deleted
inserted
replaced
125 if "not(func:same_class_paths($target_page_path, path[1]/@value))" |
125 if "not(func:same_class_paths($target_page_path, path[1]/@value))" |
126 error > Jump id="«@id»" to page "«$target_page_name»" with incompatible path "«path[1]/@value» (must be same class as "«$target_page_path»") |
126 error > Jump id="«@id»" to page "«$target_page_name»" with incompatible path "«path[1]/@value» (must be same class as "«$target_page_path»") |
127 } |
127 } |
128 } |
128 } |
129 |
129 |
130 emit "epilogue:jump" |
130 emit "declarations:jump" |
131 || |
131 || |
132 var jumps_need_update = false; |
132 var jumps_need_update = false; |
133 var jump_history = [[default_page, undefined]]; |
133 var jump_history = [[default_page, undefined]]; |
134 |
134 |
135 function update_jumps() { |
135 function update_jumps() { |