Display version #188
Display version #188
Conversation
Also, compile modes other than [Run] have --crate-type=lib so that programs without main() can easily be compiled. Lastly, add several command line options to web.py for the ease of development: the most notable are: -S for skipping playpen and -d for verbose debug output. Fix #124 Signed-off-by: NODA, Kai <[email protected]>
Signed-off-by: NODA, Kai <[email protected]>
|
Thanks for the pull request, and welcome! The Rust team is excited to review your changes, and you should hear from @nikomatsakis (or someone else) soon. If any changes to this PR are deemed necessary, please add them as extra commits. This ensures that the reviewer can see what has changed since they last reviewed the code. Due to the way GitHub handles out-of-date commits, this should also make it reasonably obvious what issues have or haven't been addressed. Large or tricky changes may require several passes of review and changes. Please see the contribution instructions for more information. |
|
The version kinda hovers over the editor, which I find a bit distracting. Can't you move it below the editor (and make the font smaller) or into the settings menu? (This might also be caused by my messed-up font setup) |
| if os.path.exists(command): | ||
| with open(command) as fp: | ||
| if re.match(r'#!.*sh', fp.readline()): | ||
| wrapper_cmd = ("sh", ) # compile.sh has non-standard #!/usr/bin/dash |
There was a problem hiding this comment.
Shouldn't you rather change the shebang instead? Not sure if that's a good idea either, but it seems better than checking in here.
There was a problem hiding this comment.
I'm not sure the Debian standard #!/bin/dash is really compatible with the playpen jail on the production server.
There was a problem hiding this comment.
According to wikipedia, Debian's /bin/sh is Dash, so you're running that anyway
There was a problem hiding this comment.
Yes it is (I'm on Debian.)
Arch is a weird distro. The tar binary package of Dash contains /usr/bin/dash but its install/uninstall hook script tweaks /etc/shells as if it's at /bin/dash. If there's really no /bin/*sh under an Arch chroot, I have to live with the above clumsiness.
The quickest solution is changing the shebang to #!/usr/bin/env sh but I think it is marginally more secure to keep using the current absolute shebang path.
There was a problem hiding this comment.
Arch symlinks /bin to /usr/bin and /sbin to /usr/sbin, so that might be what you're seeing. You should be able to use /bin/sh, since its included in bash's package.
|
@jonas-schievink As someone who never opened the config menu until today, I don't think putting the version into it is a good idea. How do you like this version? #rustc-version {
position: absolute;
font-size: 0.6em;
bottom: 2.5em;
right: 2.5em;
opacity: 0.4;
}I wish not to "waste" the precious vertical screen pixels when we often have some space at the right bottom corner of the output pane. |
|
I like that version better, neat! |
| case "$1" in | ||
| --evaluatesh=debug|--compilesh=debug) | ||
| export RUST_BACKTRACE=1 | ||
| debugme=1 |
There was a problem hiding this comment.
Is this actually used?
There was a problem hiding this comment.
Oh and the backtrace thing would be #119, so it should probably be solved in a different way (such as a check box on the website - but that can wait for another PR, too)
|
Oh wow this looks like quite a few changes all in one, can you describe in more detail what's going on here as well? |
|
Trying to split this PR to a set of independent PRs with an independent additional feature, but as someone who haven't set up Arch VM, I still think the playpen-less mode can be valuable to many potential contributors to this webapp project. |
|
It's fine to have it here for now, I'd just like a summary of what's changed. The PR title/description to not map onto the actual set of things which changed here (which is quite a lot) |
|
Ping @nodakai, want to update this? I think this is a really neat feature. |
|
Incompatible with HEAD |
Display the rustc version at the bottom right of the screen.
Try it out locally with
python3 web.py -d -Swithout playpen.