64     var url = urls.shift();
66       window.location.href = url;
70       url: url,  property
72         window.location.href = url;
82     var url = window.location.href;
83     var current_language = language_segment_from_url(url);
84     var current_version = version_segment_in_url(url);
85     var new_url = url.replace('.org/' + current_language + current_version,
87     if (new_url != url) {
90         url.replace('.org/' + current_language + current_version,
101     var url = window.location.href;
102     var current_language = language_segment_from_url(url);
103     var current_version = version_segment_in_url(url);
106     var new_url = url.replace('.org/' + current_language + current_version,
108     if (new_url != url) {
118   function language_segment_from_url(url) {  argument
120     var match = url.match(language_regexp);
128   function version_segment_in_url(url) {  argument
132     var match = url.match(version_regexp);