at 18.03-beta 31 lines 920 B view raw
1{ stdenv, fetchFromGitHub }: 2 3# To make use of this plugin, need to add 4# programs.zsh.interactiveShellInit = '' 5# source ${pkgs.zsh-command-time}/share/zsh-command-time/command-time.plugin.zsh 6# ZSH_COMMAND_TIME_MIN_SECONDS=3 7# ZSH_COMMAND_TIME_ECHO=1 8# ''; 9 10stdenv.mkDerivation rec { 11 version = "2017-05-09"; 12 name = "zsh-command-time-${version}"; 13 14 src = fetchFromGitHub { 15 owner = "popstas"; 16 repo = "zsh-command-time"; 17 rev = "2111361cbc88c542c834fbab7802ae5ae8339824"; 18 sha256 = "0hr9c7196wy9cg7vkmknszr2h446yvg9pqrq0rf3213kz074dhpg"; 19 }; 20 21 installPhase = '' 22 install -D $src/command-time.plugin.zsh --target-directory=$out/share/zsh-command-time 23 ''; 24 25 meta = with stdenv.lib; { 26 description = "Plugin that output time: xx after long commands"; 27 homepage = https://github.com/popstas/zsh-command-time; 28 license = licenses.mit; 29 platforms = platforms.unix; 30 }; 31}