or.inl and or.inr

Stream: new members

[Michael Beeson]

Post deleted, I figured out the answer myself. I only know how to delete the contents, not the whole post.

[Johan Commelin]

@Michael Beeson You can't delete posts. Only admins can.

Also... if you've figured out the answer, please consider posting the answer. Others might learn from it.