Hallihallo!
Kann man noch ein wenig abkürzen, da der Funktionsname bei einem Bookmarklet weniger relevant ist:
javascript:void((function(){p=document.getElementsByTagName('p');for(i=0;i<p.length;i++){p[i].innerHTML=p[i].innerHTML.replace(/(\[dsf (\d+)\.(\d+)\])/g,'<a href="http://dev.noctus.net/self/dsf.htm#dsf$2$3">$1</a>');}})());
Guter Einwand, werde ich mir für die Zukunft merken :-)
Darauf wird leider im entsprechenden Tipps & Tricks- Artikel nicht eingegangen, und der war bisher meine einzige Lektüre zu dem Thema...
Viele liebe Grüße,
Der Dicki