diff -r 000000000000 -r d5ce4c64ef88 Docs/ExperienceUI/pages/cmd.js --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Docs/ExperienceUI/pages/cmd.js Tue Oct 16 00:07:41 2007 -0400 @@ -0,0 +1,7 @@ +function define(name, params, desc, def) { + document.write("

"+name+" "+params+"

"+desc+"
Default: "+def+"

"); +} + +function macro(name, params, desc) { + document.write("

"+name+" "+params+"

"+desc+"

"); +}