commit 8590a1f86aff0fec62f97cbf2374fbdcd0289fce
parent b09d7d116c203b9264b9e3d42f4d3b073df5dc4d
Author: Anders Damsgaard <anders@adamsgaard.dk>
Date: Thu, 9 Apr 2020 07:46:53 +0200
Shorten randomman syntax
Diffstat:
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/.profile b/.profile
@@ -154,7 +154,7 @@ randomfile() {
}
randomman() {
- plumb "$(randomfile /usr/share/man/man[23567]/*.[23567])"
+ plumb "$(randomfile /usr/share/man/man[23567])"
}
alias julia-fast='julia --procs 1 --optimize=3 --math-mode=fast'