Hi, I used the DevFormatter 2012.0.1.38 on my WP 3.3.1 blog, it works great, also I managed to customize the look to my taste in css.
However, there’s the problem with selecting the code, which also selects line numbers in FF 12 and Opera 11 and IE 8. I need to have line numbers, so I’m looking for a solution that will not select and copy them. I’m not afraid of modyfing DevFormatter code or adding something to functions.php 🙂
I learned that GESHI has a compatibility setting, header_type. I tried editing devgeshi.php where the $this->GeSHIObj->set_header_type(GESHI_HEADER_PRE); is and changing it to GESHI_HEADER_PRE_TABLE, but to no avail.
Also, I disabled the flash header – no effect.
- The topic ‘[Plugin: Developer Formatter] Selecting code without line numbers’ is closed to new replies.