annotate public/javascripts/repository.js @ 436:4eb486dbf730 bug_169

If the remote repo URL changes, move aside the existing local mirror and start afresh.
(Not yet tested: checkpointing this prior to working on a different aspect of the problem)

function toggle_ext_url(){
	if($('repository_is_external').checked)
	    $('repository_external_url').enable();
	else
	    $('repository_external_url').disable();
}