Commit Graph

4 Commits

Author SHA1 Message Date
Robin Stocker
5468419110 servo: Merge #3612 - Allow to specify port with --devtools option (fixes #3597) (from robinst:devtools-port-option); r=jdm
Note that using `servo --devtools http://example.org` doesn't work. In
that case either the port must be specified or the option moved to the
end. But this is the same for other such options, e.g. `--profile`.

Source-Repo: https://github.com/servo/servo
Source-Revision: 9be266270b2e8d00f4cec0f1b262efce85913640
2014-10-08 08:24:36 -06:00
Matt Brubeck
010877ce85 servo: Merge #3461 - Fix misc warnings in devtools crates. r=jdm (from mbrubeck:warnings)
Source-Repo: https://github.com/servo/servo
Source-Revision: 2886fccb3eed9fa9f0d07e585d73fb74f9e8c274
2014-09-23 13:20:44 -07:00
Simon Sapin
e245f210fb servo: Merge #3438 - Upgrade Rust (from servo:rustup)
Source-Repo: https://github.com/servo/servo
Source-Revision: 045328c8e94f5bdfcd67105c5dfa9209f4cd501c
2014-09-20 15:35:08 -07:00
Josh Matthews
468a8a5fa0 servo: Merge #3172 - Dump initial prototype of devtools server into the build. Expect lies if (from jdm:devtools)
Source-Repo: https://github.com/servo/servo
Source-Revision: b82c0dced08ccda8c3c7f35643c3891bc45b058c
2014-09-19 09:15:03 -04:00