- From: Mike Sierra <letmespellitoutforyou@gmail.com>
- Date: Thu, 13 Dec 2012 14:43:14 -0500
- To: public-webplatform@w3.org
I recently used the wpd utility to push locally edited MediaWiki files to corresponding pages on the server, and found it to be extremely convenient: https://github.com/borismus/webplatform-tools To make things a little easier, I set up a corresponding scraper to get files from the server, and feel free to use it: https://github.com/mike-sierra/webplatform/blob/master/src/wpdget.pl 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