tool for local batch edits

I recently used the wpd utility to push locally edited MediaWiki files
to corresponding pages on the server, and found it to be extremely

To make things a little easier, I set up a corresponding scraper to
get files from the server, and feel free to use it:

As lightweight traffic control before pushing your edits back, it can
also check if files have been edited in the interim.

For a decent-sized task to test the workflow, I cross-referenced all
the interface & member names in the recently added Web Audio API doc.

BTW, it was unclear in the webplatform API doc how to get the same
markup you can later push back with "edit", hence the crappy scraper.

--Mike Sierra

Received on Thursday, 13 December 2012 19:43:42 UTC