diff options
| author | Vincent Laporte | 2018-10-24 11:37:19 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2018-10-24 11:54:31 +0000 |
| commit | ac613856324317543828632eaeb77ccb575c2f8f (patch) | |
| tree | 06a46c2fef806ea6d3326957c7320a7dc52c12fd /kernel/nativelib.ml | |
| parent | a95c781dadd2b4aa5a6b715cfc7238e761a807fc (diff) | |
[Manual] Fix an example
The `Undo` command is not reliable.
Diffstat (limited to 'kernel/nativelib.ml')
0 files changed, 0 insertions, 0 deletions